Polynomial.span_le_of_C_coeff_mem
theorem Polynomial.span_le_of_C_coeff_mem :
∀ {R : Type u} [inst : Semiring R] {f : Polynomial R} {I : Ideal (Polynomial R)},
(∀ (i : ℕ), Polynomial.C (f.coeff i) ∈ I) → Ideal.span {g | ∃ i, g = Polynomial.C (f.coeff i)} ≤ I
This theorem states that, given any semiring R and a polynomial `f` of type R, if every coefficient of `f` belongs to a certain ideal `I` of polynomials of R, then the ideal generated by the set of those coefficients (more specifically, the ideal generated by the set of constant polynomials derived from those coefficients) is a subset of `I`. This means that every element of the ideal spanned by these constant polynomials is also an element of the ideal `I`.
More concisely: If all coefficients of a polynomial belong to an ideal I in a semiring, then the ideal generated by the constant polynomials derived from those coefficients is contained in I.
|
Polynomial.induction_on
theorem Polynomial.induction_on :
∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Prop} (p : Polynomial R),
(∀ (a : R), M (Polynomial.C a)) →
(∀ (p q : Polynomial R), M p → M q → M (p + q)) →
(∀ (n : ℕ) (a : R), M (Polynomial.C a * Polynomial.X ^ n) → M (Polynomial.C a * Polynomial.X ^ (n + 1))) →
M p
This theorem is an induction principle for polynomials over any semiring `R`. It states that, for any property `M` of polynomials, if `M` holds for all constant polynomials (proven by `∀ (a : R), M (Polynomial.C a)`), and `M` is preserved under addition of polynomials (proven by `∀ (p q : Polynomial R), M p → M q → M (p + q)`), and `M` is preserved when multiplying a polynomial by `X` to increase its degree by 1 (proven by `∀ (n : ℕ) (a : R), M (Polynomial.C a * Polynomial.X ^ n) → M (Polynomial.C a * Polynomial.X ^ (n + 1))`), then `M` must hold for all polynomials. In other words, any property of polynomials that holds for constants, respects addition, and respects degree-increasing multiplication by `X` must hold for all polynomials.
More concisely: If a property of polynomials holds for constant polynomials and is closed under addition and degree-increasing multiplication by `X`, then it holds for all polynomials.
|
Polynomial.induction_on'
theorem Polynomial.induction_on' :
∀ {R : Type u} [inst : Semiring R] {M : Polynomial R → Prop} (p : Polynomial R),
(∀ (p q : Polynomial R), M p → M q → M (p + q)) → (∀ (n : ℕ) (a : R), M ((Polynomial.monomial n) a)) → M p
This theorem, `Polynomial.induction_on'`, states that for any type `R` equipped with a semiring structure, and any property `M` on polynomials with coefficients in `R`, to prove that a property `M` holds for all polynomials `p`, it is enough to show two things:
1. The property `M` is closed under addition, that is, if `M` holds for two polynomials `p` and `q`, then it also holds for the sum of `p` and `q`.
2. The property `M` holds for all monomials, i.e., for all polynomials of the form `a * X^n` for a coefficient `a` in `R` and a natural number `n`.
In other words, we can prove any property about polynomials by showing it's true for all monomials and also preserved under addition.
More concisely: Given a semiring `R` and a property `M` on polynomials over `R`, if `M` holds for all monomials and is closed under polynomial addition, then `M` holds for all polynomials.
|