Documentation

Mathlib.RingTheory.Adjoin.Polynomial

Polynomials and adjoining roots #

Main results #

@[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) :
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
instance Polynomial.instCommRingAdjoinSingleton {R : Type u_3} {A : Type u_4} [CommRing R] [Ring A] [Algebra R A] (x : A) :
Equations