Documentation

Mathlib.Algebra.Polynomial.Smeval

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 Algebra.Polynomial.Eval.

Main definitions #

Main results #

TODO #

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

Scalar multiplication together with taking a natural number power.

Equations
Instances For
    theorem Polynomial.smeval_def {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
    p.smeval x = p.sum (Polynomial.smul_pow x)
    @[irreducible]
    def Polynomial.smeval {R : Type u_3} [Semiring R] (p : Polynomial R) {S : Type u_4} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
    S

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

    Equations
    Instances For
      theorem Polynomial.smeval_eq_sum {R : Type u_1} [Semiring R] (p : Polynomial R) {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
      p.smeval x = p.sum (Polynomial.smul_pow x)
      @[simp]
      theorem Polynomial.smeval_C {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
      (Polynomial.C r).smeval x = r x ^ 0
      @[simp]
      theorem Polynomial.smeval_monomial {R : Type u_1} [Semiring R] (r : R) {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) (n : ) :
      ((Polynomial.monomial n) r).smeval x = r x ^ n
      theorem Polynomial.eval_eq_smeval {R : Type u_1} [Semiring R] (r : R) (p : Polynomial R) :
      Polynomial.eval r p = p.smeval r
      theorem Polynomial.eval₂_eq_smeval (R : Type u_3) [Semiring R] {S : Type u_4} [Semiring S] (f : R →+* S) (p : Polynomial R) (x : S) :
      Polynomial.eval₂ f x p = p.smeval x
      @[simp]
      theorem Polynomial.smeval_zero (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
      @[simp]
      theorem Polynomial.smeval_one (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
      @[simp]
      theorem Polynomial.smeval_X (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) :
      Polynomial.X.smeval x = x ^ 1
      @[simp]
      theorem Polynomial.smeval_X_pow (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [MulActionWithZero R S] (x : S) {n : } :
      (Polynomial.X ^ n).smeval x = 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) :
      (p + q).smeval x = p.smeval x + q.smeval x
      theorem Polynomial.smeval_natCast (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [Module R S] (x : S) (n : ) :
      (↑n).smeval x = n x ^ 0
      @[deprecated Polynomial.smeval_natCast]
      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 : ) :
      (↑n).smeval x = n x ^ 0

      Alias of Polynomial.smeval_natCast.

      @[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) :
      (r p).smeval x = r p.smeval x
      def Polynomial.smeval.linearMap (R : Type u_1) [Semiring R] {S : Type u_2} [AddCommMonoid S] [Pow S ] [Module R S] (x : S) :

      Polynomial.smeval as a linear map.

      Equations
      Instances For
        @[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 = p.smeval x
        theorem Polynomial.leval_coe_eq_smeval {R : Type u_3} [Semiring R] (r : R) :
        (Polynomial.leval r) = fun (p : Polynomial R) => p.smeval r
        @[simp]
        theorem Polynomial.smeval_neg (R : Type u_1) [Ring R] {S : Type u_2} [AddCommGroup S] [Pow S ] [Module R S] (p : Polynomial R) (x : S) :
        (-p).smeval x = -p.smeval x
        @[simp]
        theorem Polynomial.smeval_sub (R : Type u_1) [Ring R] {S : Type u_2} [AddCommGroup S] [Pow S ] [Module R S] (p : Polynomial R) (q : Polynomial R) (x : S) :
        (p - q).smeval x = p.smeval x - q.smeval x
        theorem Polynomial.smeval_neg_nat (S : Type u_3) [NonAssocRing S] [Pow S ] [NatPowAssoc S] (q : Polynomial ) (n : ) :
        q.smeval (-n) = (q.smeval (-n))

        In the module docstring for algebras at Mathlib.Algebra.Algebra.Basic, we see that [CommSemiring R] [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] is an equivalent way to express [CommSemiring R] [Semiring S] [Algebra R S] that allows one to relax the defining structures independently. For non-associative power-associative algebras (e.g., octonions), we replace the [Semiring S] with [NonAssocSemiring S] [Pow S ℕ] [NatPowAssoc S].

        theorem Polynomial.smeval_C_mul (R : Type u_1) [Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) :
        (Polynomial.C r * p).smeval x = r p.smeval x
        theorem Polynomial.smeval_at_natCast {S : Type u_2} [NonAssocSemiring S] [Pow S ] [NatPowAssoc S] (q : Polynomial ) (n : ) :
        q.smeval n = (q.smeval n)
        @[deprecated Polynomial.smeval_at_natCast]
        theorem Polynomial.smeval_at_nat_cast {S : Type u_2} [NonAssocSemiring S] [Pow S ] [NatPowAssoc S] (q : Polynomial ) (n : ) :
        q.smeval n = (q.smeval n)

        Alias of Polynomial.smeval_at_natCast.

        theorem Polynomial.smeval_at_zero (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] [NatPowAssoc S] :
        p.smeval 0 = p.coeff 0 1
        theorem Polynomial.smeval_X_mul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] :
        (Polynomial.X * p).smeval x = x * p.smeval x
        theorem Polynomial.smeval_X_pow_assoc (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (m : ) (n : ) :
        x ^ m * x ^ n * p.smeval x = x ^ m * (x ^ n * p.smeval x)
        theorem Polynomial.smeval_X_pow_mul (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ) :
        (Polynomial.X ^ n * p).smeval x = x ^ n * p.smeval x
        theorem Polynomial.smeval_monomial_mul (R : Type u_1) [Semiring R] (r : R) (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [SMulCommClass R S S] (n : ) :
        ((Polynomial.monomial n) r * p).smeval x = r (x ^ n * p.smeval x)
        theorem Polynomial.smeval_mul_X (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] :
        (p * Polynomial.X).smeval x = p.smeval x * x
        theorem Polynomial.smeval_assoc_X_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (m : ) (n : ) :
        p.smeval x * x ^ m * x ^ n = p.smeval x * (x ^ m * x ^ n)
        theorem Polynomial.smeval_mul_X_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] (n : ) :
        (p * Polynomial.X ^ n).smeval x = p.smeval x * x ^ n
        theorem Polynomial.smeval_mul (R : Type u_1) [Semiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] :
        (p * q).smeval x = p.smeval x * q.smeval x
        theorem Polynomial.smeval_pow (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] (n : ) :
        (p ^ n).smeval x = p.smeval x ^ n
        theorem Polynomial.smeval_comp (R : Type u_1) [Semiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [NonAssocSemiring S] [Module R S] [Pow S ] (x : S) [NatPowAssoc S] [IsScalarTower R S S] [SMulCommClass R S S] :
        (p.comp q).smeval x = p.smeval (q.smeval x)
        theorem Polynomial.smeval_commute_left (R : Type u_1) [Semiring R] (p : Polynomial R) {S : Type u_2} [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] {x : S} {y : S} (hc : Commute x y) :
        Commute (p.smeval x) y
        theorem Polynomial.smeval_commute (R : Type u_1) [Semiring R] (p : Polynomial R) (q : Polynomial R) {S : Type u_2} [Semiring S] [Module R S] [IsScalarTower R S S] [SMulCommClass R S S] {x : S} {y : S} (hc : Commute x y) :
        Commute (p.smeval x) (q.smeval y)
        theorem Polynomial.aeval_eq_smeval {R : Type u_1} [CommSemiring R] {S : Type u_2} [Semiring S] [Algebra R S] (x : S) (p : Polynomial R) :
        (Polynomial.aeval x) p = p.smeval x
        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) => p.smeval x