quadratic_ne_zero_of_discrim_ne_sq
theorem quadratic_ne_zero_of_discrim_ne_sq :
∀ {R : Type u_1} [inst : CommRing R] {a b c : R},
(∀ (s : R), discrim a b c ≠ s ^ 2) → ∀ (x : R), a * x * x + b * x + c ≠ 0
This theorem states that for any commutative ring `R`, and for any elements `a`, `b`, `c` of `R`, if the discriminant of the quadratic expression `ax^2 + bx + c` (computed as `b^2 - 4ac`) is not the square of any element in `R`, then the quadratic expression `ax^2 + bx + c` is not equal to zero for all `x` in `R`. In other words, the quadratic equation has no roots in the ring `R` if its discriminant does not have a square root in `R`.
More concisely: If the discriminant of the quadratic polynomial `ax^2 + bx + c` in a commutative ring `R` is not a square of any element in `R`, then the polynomial does not have a root in `R`.
|
exists_quadratic_eq_zero
theorem exists_quadratic_eq_zero :
∀ {K : Type u_1} [inst : Field K] [inst_1 : NeZero 2] {a b c : K},
a ≠ 0 → (∃ s, discrim a b c = s * s) → ∃ x, a * x * x + b * x + c = 0
This theorem states that for any field `K` (with non-zero characteristic), given any three elements `a`, `b`, and `c` from this field such that `a` is non-zero, if there exists an element `s` in the field such that the discriminant of the quadratic equation `a * x^2 + b * x + c = 0` equals `s * s` (i.e., the discriminant is a perfect square), then there exists an element `x` in the field that is a root of this quadratic equation. In other words, a quadratic equation over a field has a root if its discriminant is a perfect square in that field.
More concisely: If a quadratic polynomial `ax² + bx + c` over a non-zero characteristic field `K` has a perfect square discriminant `s²`, then there exists an element `x` in `K` such that `ax² + bx + c = 0`.
|
quadratic_eq_zero_iff_of_discrim_eq_zero
theorem quadratic_eq_zero_iff_of_discrim_eq_zero :
∀ {K : Type u_1} [inst : Field K] [inst_1 : NeZero 2] {a b c : K},
a ≠ 0 → discrim a b c = 0 → ∀ (x : K), a * x * x + b * x + c = 0 ↔ x = -b / (2 * a)
The theorem `quadratic_eq_zero_iff_of_discrim_eq_zero` states that for any field `K` with non-zero element `2`, and any elements `a`, `b`, `c` of `K` with `a` not being zero, if the discriminant of the quadratic expression `ax^2 + bx + c` equals zero, then the quadratic equation `ax^2 + bx + c = 0` implies `x` equals `-b / (2 * a)`, and vice versa. In other words, if the discriminant of a quadratic equation is zero, then the root of the equation is `-b / (2 * a)`.
More concisely: For any field `K` with non-zero element `2` and quadratic polynomial `ax² + bx + c` over `K` with `a ≠ 0`, the discriminant `b² - 4*a*c` equals zero if and only if the roots of the equation are `-b / (2*a)`.
|
quadratic_eq_zero_iff
theorem quadratic_eq_zero_iff :
∀ {K : Type u_1} [inst : Field K] [inst_1 : NeZero 2] {a b c : K},
a ≠ 0 →
∀ {s : K},
discrim a b c = s * s →
∀ (x : K), a * x * x + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
This theorem states that for any field `K` (with non-zero element 2) and any non-zero `a` in `K`, and any `b`, `c` in `K`, if the discriminant of the quadratic equation `a * x * x + b * x + c = 0` equals `s * s` for some `s` in `K`, then a solution `x` to this quadratic equation is equal to `(-b + s) / (2 * a)` or `(-b - s) / (2 * a)`. This is a formal statement of the quadratic formula in the context of an arbitrary field.
More concisely: If a quadratic polynomial `ax² + bx + c` over a field `K` with non-zero `2a` has discriminant `s²`, then its solutions are given by `(-b ± s) / (2 * a)`.
|
discrim_le_zero
theorem discrim_le_zero :
∀ {K : Type u_1} [inst : LinearOrderedField K] {a b c : K},
(∀ (x : K), 0 ≤ a * x * x + b * x + c) → discrim a b c ≤ 0
This theorem states that if a degree 2 polynomial with coefficients from a linearly ordered field is always nonnegative for all values of the variable, then the discriminant of the polynomial is less than or equal to zero. The discriminant of a quadratic equation is calculated as the square of the second coefficient minus four times the product of the first and third coefficients. This theorem is used to establish the relationship between the nature of the roots of the quadratic equation (real or complex) and whether the entire polynomial is always nonnegative.
More concisely: If a quadratic polynomial over a linearly ordered field has only non-negative roots, then its discriminant is non-positive.
|
discrim_lt_zero
theorem discrim_lt_zero :
∀ {K : Type u_1} [inst : LinearOrderedField K] {a b c : K},
a ≠ 0 → (∀ (x : K), 0 < a * x * x + b * x + c) → discrim a b c < 0
This theorem states that if we have a degree 2 polynomial, which is always positive for all real numbers, then its discriminant is negative, provided that the coefficient of the quadratic term is not zero. In mathematical language, for a polynomial of the form \(ax^2 + bx + c\), where \(a \neq 0\) and for all \(x\) in the field \(a * x * x + b * x + c > 0\), the discriminant of the polynomial, given by \(b^2 - 4ac\), is less than zero.
More concisely: If a degree 2 polynomial \(ax^2 + bx + c\) with non-zero coefficient \(a\) is always positive for all real numbers, then its discriminant \(b^2 - 4ac\) is negative.
|
quadratic_eq_zero_iff_discrim_eq_sq
theorem quadratic_eq_zero_iff_discrim_eq_sq :
∀ {R : Type u_1} [inst : CommRing R] {a b c : R} [inst_1 : NeZero 2] [inst_2 : NoZeroDivisors R],
a ≠ 0 → ∀ (x : R), a * x * x + b * x + c = 0 ↔ discrim a b c = (2 * a * x + b) ^ 2
This theorem states that for any commutative ring `R` with no zero divisors and non-zero element `2`, a quadratic equation `ax^2 + bx + c = 0` (where `a` is not equal to `0`) has roots if and only if the discriminant of the quadratic, given by `b^2 - 4ac`, equals the square of `2ax + b`. In essence, this theorem gives a condition for a quadratic equation to have roots in terms of the discriminant and the coefficients of the quadratic equation.
More concisely: A quadratic equation `ax^2 + bx + c = 0` (where `a ≠ 0` and `R` is a commutative ring with no zero divisors and non-zero element `2`) has roots if and only if the discriminant `b^2 - 4ac` equals `(2añ)^2`.
|