Polynomials and adjoining roots

Main results

• Algebra.instCommSemiringAdjoinSingleton, Algebra.instCommRingAdjoinSingleton: adjoining an element to a commutative (semi)ring gives a commutative (semi)ring
• Algebra.adjoin_singleton_induction: proving a fact about a : adjoin R {x} is the same as proving it for aeval x p where p is an arbitrary polynomial

@[simp]

theorem Polynomial.adjoin_X {R : Type u} [CommSemiring R] : R[X] = ⊤

theorem Algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : R[x] = (Polynomial.aeval x).range

@[simp]

theorem Polynomial.aeval_mem_adjoin_singleton (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] {p : Polynomial R} (x : A) : (aeval x) p ∈ R[x]

theorem Algebra.adjoin_mem_exists_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {a : A} (h : a ∈ R[x]) : ∃ (p : Polynomial R), (Polynomial.aeval x) p = a

theorem Algebra.adjoin_eq_exists_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) (a : ↥R[x]) : ∃ (p : Polynomial R), (Polynomial.aeval x) p = ↑a

theorem Algebra.adjoin_singleton_induction (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) {M : ↥R[x] → Prop} (a : ↥R[x]) (f : ∀ (p : Polynomial R), M ⟨(Polynomial.aeval x) p, ⋯⟩) : M a

Proving a fact about a : adjoin R {x} is the same as proving it for aeval x p where pis an arbitrary polynomial.

@[implicit_reducible]

instance Algebra.instCommSemiringAdjoinSingleton (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : CommSemiring ↥R[x]

@[implicit_reducible]

instance Algebra.instCommRingAdjoinSingleton {R : Type u_3} {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] (x : A) : CommRing ↥R[x]