Scalar-multiple polynomial evaluation

This file defines polynomial evaluation via scalar multiplication. Our polynomials have coefficients in a semiring R, and we evaluate at a weak form of R-algebra, namely an additive commutative monoid with an action of R and a notion of natural number power. This is a generalization of Data.Polynomial.Eval.

Main definitions

• Polynomial.smeval: function for evaluating a polynomial with coefficients in a Semiring R at an element x of an AddCommMonoid S that has natural number powers and an R-action.

To do

• smeval_neg and smeval_int_cast for R a ring and S an AddCommGroup.
• smeval_mul, smeval_comp, etc. for R commutative, S a power-associative non-assoc. R-alg.
• smeval.algebraMap def and aeval = smeval.algebraMap theorem.
• Nonunital evaluation for polynomials with vanishing constant term for Pow S ℕ+ (different file?)

def Polynomial.smul_pow {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_2} [Semiring R] [MulActionWithZero R S] : ℕ → R → S

Scalar multiplication together with taking a natural number power.

Equations

• Polynomial.smul_pow x n r = r • x ^ n

@[irreducible]

def Polynomial.smeval {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_3} [Semiring R] [MulActionWithZero R S] (p : Polynomial R) : S

Evaluate a polynomial p in the scalar commutative semiring R at an element x in the target S using scalar multiple R-action.

Equations

• @Polynomial.smeval = Polynomial.wrapped✝.1

theorem Polynomial.smeval_def {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_3} [Semiring R] [MulActionWithZero R S] (p : Polynomial R) : Polynomial.smeval x p = Polynomial.sum p (Polynomial.smul_pow x)

theorem Polynomial.smeval_eq_sum {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_2} [Semiring R] [MulActionWithZero R S] (p : Polynomial R) : Polynomial.smeval x p = Polynomial.sum p (Polynomial.smul_pow x)

@[simp]

theorem Polynomial.smeval_zero {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) (R : Type u_2) [Semiring R] [MulActionWithZero R S] : Polynomial.smeval x 0 = 0

@[simp]

theorem Polynomial.smeval_C {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_2} [Semiring R] [MulActionWithZero R S] (r : R) : Polynomial.smeval x (Polynomial.C r) = r • x ^ 0

@[simp]

theorem Polynomial.smeval_one {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) (R : Type u_2) [Semiring R] [MulActionWithZero R S] : Polynomial.smeval x 1 = 1 • x ^ 0

@[simp]

theorem Polynomial.smeval_X {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) (R : Type u_2) [Semiring R] [MulActionWithZero R S] : Polynomial.smeval x Polynomial.X = x ^ 1

@[simp]

theorem Polynomial.smeval_monomial {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) {R : Type u_2} [Semiring R] [MulActionWithZero R S] (r : R) (n : ℕ) : Polynomial.smeval x ((Polynomial.monomial n) r) = r • x ^ n

@[simp]

theorem Polynomial.smeval_X_pow {S : Type u_1} [AddCommMonoid S] [Pow S ℕ] (x : S) (R : Type u_2) [Semiring R] [MulActionWithZero R S] {n : ℕ} : Polynomial.smeval x (Polynomial.X ^ n) = x ^ n

@[simp]

theorem Polynomial.smeval_add (R : Type u_1) [Semiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : Polynomial.smeval x (p + q) = Polynomial.smeval x p + Polynomial.smeval x q

theorem Polynomial.smeval_nat_cast (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (n : ℕ) : Polynomial.smeval x ↑n = n • x ^ 0

@[simp]

theorem Polynomial.smeval_smul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) (r : R) : Polynomial.smeval x (r • p) = r • Polynomial.smeval x p

def Polynomial.smeval.linearMap (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : Polynomial R →ₗ[R] S

Polynomial.smeval as a linear map.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Polynomial.smeval.linearMap_apply (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ℕ] [Module R S] (x : S) : (Polynomial.smeval.linearMap R x) p = Polynomial.smeval x p

theorem Polynomial.eval₂_eq_smeval (R : Type u_1) [Semiring R] {S : Type u_2} [Semiring S] (f : R →+* S) (p : Polynomial R) (x : S) : Polynomial.eval₂ f x p = Polynomial.smeval x p

theorem Polynomial.leval_coe_eq_smeval {R : Type u_1} [Semiring R] (r : R) : ⇑(Polynomial.leval r) = fun (p : Polynomial R) => Polynomial.smeval r p

theorem Polynomial.leval_eq_smeval {R : Type u_1} [Semiring R] (r : R) : Polynomial.leval r = Polynomial.smeval.linearMap R r

theorem Polynomial.aeval_coe_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) : ⇑(Polynomial.aeval x) = fun (p : Polynomial R) => Polynomial.smeval x p