Polynomial.smeval_eq_sum
theorem Polynomial.smeval_eq_sum :
∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
[inst_3 : MulActionWithZero R S] (x : S), p.smeval x = p.sum (Polynomial.smul_pow x)
The theorem `Polynomial.smeval_eq_sum` states that for a given polynomial `p` from a semiring `R` and an element `x` from an additive commutative monoid `S` that is also equipped with a power operation and a scalar multiplication with zero, the operation of evaluating the polynomial at `x` is equivalent to summing the values of the function, which applies scalar multiplication and natural number power to `x`, on the coefficients of the polynomial `p`. In mathematical terms, if `p` is a polynomial with coefficients in `R` and `x` is in `S`, then the value of `p` at `x` is equal to the sum over all coefficients of `p` of the value at that coefficient times `x` to the power of the corresponding exponent.
More concisely: For a polynomial $p$ with coefficients in a semiring $R$ and an element $x$ from an additive commutative monoid $S$ with power operation and scalar multiplication with zero, the value of $p$ at $x$ equals the sum of the products of coefficients and $x$ raised to the corresponding exponent.
|
Polynomial.smeval_def
theorem Polynomial.smeval_def :
∀ {R : Type u_3} [inst : Semiring R] (p : Polynomial R) {S : Type u_4} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
[inst_3 : MulActionWithZero R S] (x : S), p.smeval x = p.sum (Polynomial.smul_pow x)
The theorem `Polynomial.smeval_def` states that for any semiring `R`, polynomial `p` over `R`, and for any type `S` forming an additive commutative monoid with a power operation and a scalar multiplication with zero, the evaluation of the polynomial `p` at an element `x` of `S` (`Polynomial.smeval p x`) is equal to the sum of the function applied to the coefficients of the polynomial `p` where the function is the scalar multiplication of the coefficient to the power of its corresponding term index (`Polynomial.sum p (Polynomial.smul_pow x)`). In essence, this theorem links polynomial evaluation with summing over scalar multiplication and powers, given specific algebraic structures.
More concisely: For any semiring `R`, polynomial `p` over `R`, and type `S` with additive commutative monoid, power operation, and scalar multiplication with zero, the evaluation of polynomial `p` at an element `x` of `S` equals the sum of the scalar multiplication of the coefficient by the power of its term index. (i.e., `Polynomial.smeval p x = Polynomial.sum p (Polynomial.smul_pow x)`)
|
Polynomial.smeval_add
theorem Polynomial.smeval_add :
∀ (R : Type u_1) [inst : Semiring R] (p q : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S]
[inst_2 : Pow S ℕ] [inst_3 : Module R S] (x : S), (p + q).smeval x = p.smeval x + q.smeval x
The theorem `Polynomial.smeval_add` states that for any semiring `R`, given two polynomials `p` and `q` over `R`, and a scalar `x` from a type `S` that has an additive commutative monoid structure, a power operation, and is a module over `R`, the evaluation of the sum of `p` and `q` at `x` is equal to the sum of the evaluations of `p` and `q` at `x`. In mathematical terms, if we denote the `Polynomial.smeval` operation as $f$, this theorem is stating that $f(p + q, x) = f(p, x) + f(q, x)$ for all polynomials $p, q$ and scalars $x$.
More concisely: For any semiring `R`, given polynomials `p` and `q` over `R` and a scalar `x` from an additive commutative monoid with power operation and `R`-module structure, `Polynomial.smeval (p + q) x = Polynomial.smeval p x + Polynomial.smeval q x`.
|