Polynomials and adjoining roots

Main results

• Polynomial.instCommSemiringAdjoinSingleton, instCommRingAdjoinSingleton: adjoining an element to a commutative (semi)ring gives a commutative (semi)ring

@[simp]

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

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

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

Equations

• Polynomial.instCommSemiringAdjoinSingleton R x = CommSemiring.mk ⋯

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

Equations

• Polynomial.instCommRingAdjoinSingleton x = CommRing.mk ⋯