Cubic.map_toPoly
theorem Cubic.map_toPoly :
∀ {R : Type u_1} {S : Type u_2} {P : Cubic R} [inst : Semiring R] [inst_1 : Semiring S] {φ : R →+* S},
(Cubic.map φ P).toPoly = Polynomial.map φ P.toPoly
The theorem `Cubic.map_toPoly` states that for all semirings `R` and `S`, a cubic polynomial `P` over `R`, and a semiring homomorphism `φ` from `R` to `S`, mapping `P` to `S` using `φ` and then converting to a polynomial is the same as first converting `P` to a polynomial and then mapping the polynomial to `S` using `φ`. In mathematical terms, if we denote the conversion of a cubic polynomial to a polynomial as `Cubic.toPoly` and mapping across a semiring homomorphism as `.map`, we have that `Cubic.toPoly (Cubic.map φ P) = Polynomial.map φ (Cubic.toPoly P)`.
More concisely: For all semirings R, S, a cubic polynomial P over R, and a semiring homomorphism φ from R to S, the conversion of the map of P under φ to a polynomial in S is equal to the map of the polynomial obtained from converting P to S. That is, (Cubic.map φ (Cubic.toPoly P)) = (Polynomial.map φ (Cubic.toPoly P)).
|
Cubic.of_b_eq_zero
theorem Cubic.of_b_eq_zero :
∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R],
P.a = 0 → P.b = 0 → P.toPoly = Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
This theorem states that for any semiring `R`, and any cubic polynomial `P` over `R`, if the coefficients of `x^3` and `x^2` terms (`P.a` and `P.b`) in `P` are zero, then the polynomial obtained by converting the cubic polynomial `P` to a general polynomial is equivalent to `P.c * x + P.d`. In other words, if a cubic polynomial lacks `x^3` and `x^2` terms, it behaves exactly like a linear polynomial.
More concisely: If `P` is a cubic polynomial over a semiring with zero coefficients for `x^3` and `x^2` terms, then `P` is equivalent to `P.c * x + P.d`.
|
Cubic.of_a_eq_zero
theorem Cubic.of_a_eq_zero :
∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R],
P.a = 0 → P.toPoly = Polynomial.C P.b * Polynomial.X ^ 2 + Polynomial.C P.c * Polynomial.X + Polynomial.C P.d
This theorem, `Cubic.of_a_eq_zero`, states that for any type `R` that is a semiring and a cubic polynomial `P` of type `R`, if the coefficient of the cubic term `P.a` is zero, then the cubic polynomial is equivalent to the polynomial comprised of the remaining terms. Specifically, this polynomial is constructed by multiplying the coefficient of the quadratic term `P.b` by `X` squared, adding the product of the linear term coefficient `P.c` and `X`, and finally adding the constant term `P.d`. This polynomial is achieved by applying the `Polynomial.C` function to each of the coefficients.
More concisely: If the cubic coefficient of a polynomial P over a semiring R is zero, then P is equivalent to the quadratic polynomial obtained by multiplying the quadratic coefficient by X^2, adding the linear coefficient times X, and adding the constant coefficient.
|
Cubic.eq_sum_three_roots
theorem Cubic.eq_sum_three_roots :
∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K} {x y z : K},
P.a ≠ 0 →
(Cubic.map φ P).roots = {x, y, z} →
Cubic.map φ P =
{ a := φ P.a, b := φ P.a * -(x + y + z), c := φ P.a * (x * y + x * z + y * z),
d := φ P.a * -(x * y * z) }
The theorem `Cubic.eq_sum_three_roots` states that given two fields `F` and `K`, a cubic polynomial `P` in field `F`, a ring homomorphism `φ` from `F` to `K`, and three elements `x`, `y`, and `z` in field `K`, if the leading coefficient of `P` is non-zero and the roots of the cubic polynomial `P` mapped to `K` are `x`, `y`, and `z`, then the mapped cubic polynomial can be expressed in terms of the coefficients of `P` and the roots `x`, `y`, and `z`. Specifically, the coefficients of the mapped cubic polynomial are `φ(P.a)`, `φ(P.a) * -(x + y + z)`, `φ(P.a) * (x * y + x * z + y * z)`, and `φ(P.a) * -(x * y * z)`, respectively.
More concisely: Given a field extension `φ: F → K`, a non-zero cubic polynomial `P` over `F` with roots `x`, `y`, and `z` in `K`, the coefficients of the mapped cubic polynomial are `φ(P.a)`, `φ(P.a) * (-(x + y + z))`, `φ(P.a) * (xy + xz + yz)`, and `φ(P.a) * (-xyz)`.
|
Cubic.leadingCoeff_of_a_ne_zero
theorem Cubic.leadingCoeff_of_a_ne_zero :
∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a ≠ 0 → P.toPoly.leadingCoeff = P.a
The theorem `Cubic.leadingCoeff_of_a_ne_zero` states that for any type `R` and any cubic polynomial `P` of type `Cubic R`, under the condition that there is a semiring structure on `R` and the coefficient `P.a` of the cubic term in `P` is non-zero, the leading coefficient of the polynomial obtained by converting `P` to a polynomial using the `Cubic.toPoly` function is equal to `P.a`.
More concisely: Given a cubic polynomial `P` over a semiring `R` with non-zero cubic coefficient `P.a`, the leading coefficient of `Cubic.toPoly P` equals `P.a`.
|
Cubic.of_c_eq_zero
theorem Cubic.of_c_eq_zero :
∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.c = 0 → P.toPoly = Polynomial.C P.d := by
sorry
The theorem `Cubic.of_c_eq_zero` states that for any type `R` that is a semiring and any cubic polynomial `P` of type `R`, if the coefficients `a`, `b`, and `c` of `P` are all zero, then the conversion of `P` to a regular polynomial using `Cubic.toPoly` is equal to a constant polynomial with coefficient `d`. In other words, a cubic polynomial with all coefficients except the constant term being zero is just a constant polynomial in the semiring `R`.
More concisely: For any semiring `R` and cubic polynomial `P` over `R` with coefficients `a`, `b`, and `c` such that `a = b = 0`, the conversion of `P` to a regular polynomial using `Cubic.toPoly` is equal to the constant polynomial with coefficient `c`.
|