Polynomial.mem_annIdeal_iff_aeval_eq_zero
theorem Polynomial.mem_annIdeal_iff_aeval_eq_zero :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {a : A}
{p : Polynomial R}, p ∈ Polynomial.annIdeal R a ↔ (Polynomial.aeval a) p = 0
This theorem states that for any commutative semiring `R`, semiring `A`, algebra structure between `R` and `A`, element `a` of `A`, and polynomial `p` with coefficients in `R`, the polynomial `p` is in the annihilating ideal of `a` (denoted as `Polynomial.annIdeal R a`) if and only if the result of applying the algebraic evaluation map `Polynomial.aeval a` to `p` is zero. Informally, this means that a polynomial is in the set of polynomials that, when evaluated at `a`, yield zero if and only if that polynomial indeed evaluates to zero at `a`.
More concisely: For any commutative semiring R, semiring A, algebra structure over R on A, element a in A, and polynomial p with coefficients in R, p is in the annihilator ideal of a if and only if aeval a p = 0.
|
Polynomial.degree_annIdealGenerator_le_of_mem
theorem Polynomial.degree_annIdealGenerator_le_of_mem :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
∀ p ∈ Polynomial.annIdeal 𝕜 a, p ≠ 0 → (Polynomial.annIdealGenerator 𝕜 a).degree ≤ p.degree
The theorem states that, given a Field 𝕜, a Ring A, and an element 'a' of A, for any non-zero polynomial 'p' that belongs to the annihilating ideal of 'a', the degree of the generator of the annihilating ideal is less than or equal to the degree of 'p'. The annihilating ideal of 'a' is the set of all polynomials that evaluate to zero at 'a', and its generator is a monic polynomial that generates the ideal. This theorem basically states that this generator has the smallest degree among all non-zero polynomials in the ideal.
More concisely: Given a field 𝕜, a ring A, and an element a of A, the degree of the monic generator of the annihilating ideal of a is less than or equal to the degree of any non-zero polynomial in the ideal that annihilates a.
|
Polynomial.annIdealGenerator_mem
theorem Polynomial.annIdealGenerator_mem :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
Polynomial.annIdealGenerator 𝕜 a ∈ Polynomial.annIdeal 𝕜 a
The theorem states that for any field 𝕜, ring A, and algebra 𝕜 A, and for any element 'a' of A, the annihilating ideal generator of 'a' is a member of the annihilating ideal of 'a'. This means that the polynomial that generates the annihilating ideal for a given element – that is, the polynomial that, when evaluated at that element gives zero, is itself in the annihilating ideal. Here, the annihilating ideal of an element is the set of all polynomials that evaluate to zero at that element.
More concisely: For any field 𝕜, ring A, and algebra 𝕜-module M over it, the generator of the annihilating ideal of an element 'a' in M lies in the annihilating ideal of 'a'.
|
Polynomial.annIdealGenerator_eq_zero_iff
theorem Polynomial.annIdealGenerator_eq_zero_iff :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] {a : A},
Polynomial.annIdealGenerator 𝕜 a = 0 ↔ Polynomial.annIdeal 𝕜 a = ⊥
This theorem states that for any field `𝕜`, ring `A`, and algebra structure over `𝕜` and `A`, and for any element `a` in `A`, the monic generator of the annihilating ideal of `a` is zero if and only if the annihilating ideal of `a` is the zero ideal. Here, the annihilating ideal of `a` is the set of all polynomials `p` in `𝕜[X]` such that when `p` is evaluated at `a`, the result is zero. The monic generator of this ideal is a specific polynomial `g` such that the principal ideal generated by `g` is equal to the annihilating ideal, and `g` is chosen to be monic if possible. The zero ideal, denoted by `⊥`, is the ideal that contains only the zero polynomial.
More concisely: For any field `𝕜`, ring `A`, and algebra structure over `𝕜` and `A`, the monic generator of the annihilating ideal of an element `a` in `A` is zero if and only if the annihilating ideal of `a` is the zero ideal.
|
Polynomial.annIdealGenerator_eq_minpoly
theorem Polynomial.annIdealGenerator_eq_minpoly :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
Polynomial.annIdealGenerator 𝕜 a = minpoly 𝕜 a
The theorem `Polynomial.annIdealGenerator_eq_minpoly` states that for any field `𝕜`, a ring `A` and an element `a` of `A`, the generator of the annihilating ideal of `a` over `𝕜` is equal to the minimal polynomial of `a` over `𝕜`. In other words, the polynomial which generates the ideal of all polynomials that annihilate `a` when evaluated at `a` is the same as the minimal polynomial of `a`, the smallest degree monic polynomial with coefficients in `𝕜` such that evaluating it at `a` gives zero.
More concisely: The generator of the annihilating ideal of an element `a` in a ring `A` over a field `𝕜` is equal to the minimal polynomial of `a` over `𝕜`.
|
Polynomial.monic_generator_eq_minpoly
theorem Polynomial.monic_generator_eq_minpoly :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A)
(p : Polynomial 𝕜), p.Monic → Ideal.span {p} = Polynomial.annIdeal 𝕜 a → Polynomial.annIdealGenerator 𝕜 a = p
This theorem states that for any field `𝕜`, ring `A`, algebra structure `𝕜 A`, and element `a` of `A`, if a monic polynomial `p` of `𝕜` generates the annihilating ideal of `a` (i.e., the ideal formed by all polynomials that, when evaluated at `a`, yield zero), then `p` must be the same as the polynomial returned by the `annIdealGenerator` function for `a`. In other words, if the polynomial `p` generates the annihilating ideal of `a` under the condition that it's monic, then the `annIdealGenerator` function, which produces a monic generator of the annihilating ideal, must yield `p`.
More concisely: If a monic polynomial generates the annihilating ideal of an element in a ring with an algebra structure over a field, then it is the same polynomial as the monic generator returned by the `annIdealGenerator` function for that element.
|
Polynomial.span_singleton_annIdealGenerator
theorem Polynomial.span_singleton_annIdealGenerator :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
Ideal.span {Polynomial.annIdealGenerator 𝕜 a} = Polynomial.annIdeal 𝕜 a
The theorem `Polynomial.span_singleton_annIdealGenerator` asserts that for any field `𝕜`, ring `A`, and algebra `𝕜 A` with an element `a` in `A`, the ideal generated by the singleton set containing the annihilating ideal's monic generator for `a` is equal to the annihilating ideal of `a` itself. In simpler terms, it states that the annihilating polynomial (a polynomial which when evaluated at `a` results in zero), if it exists, generates the same ideal as the annihilating ideal of `a`.
More concisely: For any field `𝕜`, ring `A`, and algebra `𝕜 A` with `a` in `A`, the ideal generated by the monic annihilator of `a` is equal to the annihilating ideal of `a`.
|
Polynomial.monic_annIdealGenerator
theorem Polynomial.monic_annIdealGenerator :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : Field 𝕜] [inst_1 : Ring A] [inst_2 : Algebra 𝕜 A] (a : A),
Polynomial.annIdealGenerator 𝕜 a ≠ 0 → (Polynomial.annIdealGenerator 𝕜 a).Monic
This theorem asserts that for any field `𝕜` and ring `A` equipped with an algebra structure over `𝕜`, and for any element `a` of `A`, if the polynomial `annIdealGenerator` relative to `𝕜` and `a` is not zero, then it is monic. Here, being monic means that the polynomial's leading coefficient is one. An `annIdealGenerator` of an element `a` in `A` is a monic generator of the ideal of all polynomials that annihilate `a` (meaning when they act on `a`, they yield zero). This theorem is particularly concerning the case when the annihilating ideal is not zero.
More concisely: For any field `𝕜` and ring `A` with an algebra structure over `𝕜`, if `a` is an element of `A` such that the annihilating ideal generated by a monic polynomial `p` is non-zero, then `p` is monic itself.
|