Polynomials and adjoining roots #
Main results #
Polynomial.instCommSemiringAdjoinSingleton, instCommRingAdjoinSingleton
: adjoining an element to a commutative (semi)ring gives a commutative (semi)ring
theorem
Algebra.adjoin_singleton_eq_range_aeval
(R : Type u)
{A : Type z}
[CommSemiring R]
[Semiring A]
[Algebra R A]
(x : A)
:
@[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)
: