Polynomial.IsUnitTrinomial.irreducible_of_coprime'
theorem Polynomial.IsUnitTrinomial.irreducible_of_coprime' :
∀ {p : Polynomial ℤ},
p.IsUnitTrinomial →
(∀ (z : ℂ), ¬((Polynomial.aeval z) p = 0 ∧ (Polynomial.aeval z) p.mirror = 0)) → Irreducible p
This theorem states that for any unit trinomial `p`, which is a polynomial with integer coefficients, if `p` does not have any complex roots in common with its mirror (the polynomial obtained by reversing the order of its coefficients), then `p` is irreducible. Here, a root is considered common if the values of `p` and its mirror both vanish at that complex number `z`, as determined by the algebra homomorphism `Polynomial.aeval z`. The theorem essentially links the irreducibility of a unit trinomial with the distinctness of its roots and those of its mirror in the complex plane.
More concisely: If a unit trinomial `p` with integer coefficients has no complex roots in common with its mirror, then `p` is irreducible.
|
Polynomial.IsUnitTrinomial.irreducible_of_isCoprime
theorem Polynomial.IsUnitTrinomial.irreducible_of_isCoprime :
∀ {p : Polynomial ℤ}, p.IsUnitTrinomial → IsCoprime p p.mirror → Irreducible p
This theorem states that, given a trinomial `p` which is a unit, if `p` is coprime with its mirror (i.e., there exist integers `a` and `b` such that `a * p + b * p.mirror = 1`), then `p` is irreducible. In the context of polynomials, "irreducible" means that the polynomial cannot be factored into a product of two non-unit polynomials, and "unit trinomial" refers to a trinomial where the leading coefficient is a unit of the ring of integers. The "mirror" of a polynomial is another polynomial obtained by reversing the order of its coefficients.
More concisely: If a unit trinomial `p(x)` is coprime with its mirror `p.mirror(x)`, then `p(x)` is irreducible.
|
Polynomial.trinomial_def
theorem Polynomial.trinomial_def :
∀ {R : Type u_1} [inst : Semiring R] (k m n : ℕ) (u v w : R),
Polynomial.trinomial k m n u v w =
Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ m + Polynomial.C w * Polynomial.X ^ n
The theorem `Polynomial.trinomial_def` states that for any semiring `R`, any natural numbers `k`, `m`, `n`, and any elements `u`, `v`, `w` of `R`, the trinomial polynomial function, `Polynomial.trinomial k m n u v w`, is equivalent to a sum of three terms: the first term is the constant `u` times `X` to the power of `k`, the second term is the constant `v` times `X` to the power of `m`, and the third term is the constant `w` times `X` to the power of `n`. Here, `Polynomial.C` is a ring homomorphism that maps an element of `R` to its corresponding constant polynomial, and `Polynomial.X` is the polynomial variable.
More concisely: For any semiring `R`, `Polynomial.trinomial k m n u v w` equals the sum of `u * X^k`, `v * X^m`, and `w * X^n`, where `Polynomial.C(u)`, `Polynomial.C(v)`, and `Polynomian.C(w)` are the constant polynomials corresponding to `u`, `v`, and `w`, respectively, and `Polynomial.X` is the polynomial variable.
|