English
There is a canonical endomorphism of MvPolynomial that expands a polynomial by raising each variable to the p-th power, in a way compatible with the algebra structure.
Русский
Существует канонический эндоморфизм MvPolynomial, который расширяет полином, возводя переменные в p-ую степень, согласованный с алгебраической структурой.
LaTeX
$$$$ \text{expand}(p) : MvPolynomial(\sigma,R) \to MvPolynomial(\sigma,R)$$$$
Lean4
/-- Expand the polynomial by a factor of p, so `∑ aₙ xⁿ` becomes `∑ aₙ xⁿᵖ`.
See also `Polynomial.expand`. -/
noncomputable def expand (p : ℕ) : MvPolynomial σ R →ₐ[R] MvPolynomial σ R :=
{ (eval₂Hom C fun i ↦ X i ^ p : MvPolynomial σ R →+* MvPolynomial σ R) with commutes' := fun _ ↦ eval₂Hom_C _ _ _ }
