Evaluating polynomials and scalar multiplication

Main results

• eval₂_smul, eval_smul, map_smul, comp_smul: the functions preserve scalar multiplication
• Polynomial.leval: Polynomial.eval as linear map

@[simp]

theorem Polynomial.eval₂_smul {R : Type u} {S : Type v} [Semiring R] [Semiring S] (g : R →+* S) (p : Polynomial R) (x : S) {s : R} : Polynomial.eval₂ g x (s • p) = g s * Polynomial.eval₂ g x p

@[simp]

theorem Polynomial.eval_smul {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p : Polynomial R) (x : R) : Polynomial.eval x (s • p) = s • Polynomial.eval x p

def Polynomial.leval {R : Type u_1} [Semiring R] (r : R) : Polynomial R →ₗ[R] R

Polynomial.eval as linear map

Equations

• Polynomial.leval r = { toFun := fun (f : Polynomial R) => Polynomial.eval r f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Polynomial.leval_apply {R : Type u_1} [Semiring R] (r : R) (f : Polynomial R) : (Polynomial.leval r) f = Polynomial.eval r f

@[simp]

theorem Polynomial.smul_comp {R : Type u} {S : Type v} [Semiring R] [Monoid S] [DistribMulAction S R] [IsScalarTower S R R] (s : S) (p q : Polynomial R) : (s • p).comp q = s • p.comp q

@[simp]

theorem Polynomial.map_smul {R : Type u} {S : Type v} [Semiring R] {p : Polynomial R} [Semiring S] (f : R →+* S) (r : R) : Polynomial.map f (r • p) = f r • Polynomial.map f p