Polynomial.smul_eq_map
theorem Polynomial.smul_eq_map :
∀ {M : Type u_1} [inst : Monoid M] (R : Type u_2) [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M),
HSMul.hSMul m = Polynomial.map (MulSemiringAction.toRingHom M R m)
The theorem `Polynomial.smul_eq_map` states that for any monoid `M`, semiring `R`, and a multiplication action of `M` on `R`, every element `m` of `M` induces a semiring homomorphism that maps a polynomial over `R` to a polynomial over `R`, and this homomorphism is equivalent to the left action of `m` on a polynomial. In other words, the scalar multiplication of a polynomial by `m` is the same as mapping the polynomial across a ring homomorphism defined by the action of `m`.
More concisely: For any monoid action on a semiring, the induced homomorphism from an element in the monoid maps polynomials over the semiring to polynomials over the semiring, and this homomorphism is equal to the left multiplication by the element on polynomials.
|
Polynomial.smul_X
theorem Polynomial.smul_X :
∀ {M : Type u_1} [inst : Monoid M] {R : Type u_2} [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] (m : M),
m • Polynomial.X = Polynomial.X
The theorem `Polynomial.smul_X` states that for any type `M` equipped with a monoid structure, any type `R` equipped with a semiring structure, any action of `M` on `R` preserving the semiring operations (i.e., a `MulSemiringAction`), and any element `m` of `M`, the polynomial obtained by scalar multiplication of the polynomial variable (also known as the indeterminate, represented by `Polynomial.X`) by `m` is equal to the original polynomial variable `Polynomial.X`. In short, it asserts that scalar multiplication by any element of the monoid leaves the polynomial variable `Polynomial.X` unchanged.
More concisely: For any monoid `M`, semiring `R`, `MulSemiringAction` `mul_action` of `M` on `R`, and `m` in `M`, `Polynomial.X * mul_action m = Polynomial.X` holds in the polynomial ring over `R`.
|