Evaluation of polynomials in an algebra #
This file concerns evaluating polynomials where the map is algebraMap
TODO: merge with parts of Algebra/Polynomial/AlgebraMap.lean?
@[simp]
theorem
Polynomial.eval₂_mul'
{R : Type u}
{S : Type v}
[CommSemiring R]
[Semiring S]
[Algebra R S]
(x : S)
(p q : Polynomial R)
:
Polynomial.eval₂ (algebraMap R S) x (p * q) = Polynomial.eval₂ (algebraMap R S) x p * Polynomial.eval₂ (algebraMap R S) x q
@[simp]
theorem
Polynomial.eval₂_pow'
{R : Type u}
{S : Type v}
[CommSemiring R]
[Semiring S]
[Algebra R S]
(x : S)
(p : Polynomial R)
(n : ℕ)
:
Polynomial.eval₂ (algebraMap R S) x (p ^ n) = Polynomial.eval₂ (algebraMap R S) x p ^ n
@[simp]
theorem
Polynomial.eval₂_comp'
{R : Type u}
{S : Type v}
[CommSemiring R]
[Semiring S]
[Algebra R S]
(x : S)
(p q : Polynomial R)
:
Polynomial.eval₂ (algebraMap R S) x (p.comp q) = Polynomial.eval₂ (algebraMap R S) (Polynomial.eval₂ (algebraMap R S) x q) p