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] : Algebra.adjoin R {X} = ⊤

theorem Algebra.adjoin_singleton_eq_range_aeval (R : Type u) {A : Type z} [CommSemiring R] [Semiring A] [Algebra R A] (x : A) : adjoin 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 ∈ Algebra.adjoin 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 ∈ adjoin 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 : ↥(adjoin 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 : ↥(adjoin R {x}) → Prop} (a : ↥(adjoin 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 ↥(adjoin R {x})

Equations

• Algebra.instCommSemiringAdjoinSingleton R x = { toSemiring := (Algebra.adjoin R {x}).toSemiring, mul_comm := ⋯ }

@[implicit_reducible]

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

Equations

• Algebra.instCommRingAdjoinSingleton x = { toRing := (Algebra.adjoin R {x}).toRing, mul_comm := ⋯ }