English
verschiebung is an additive monoid hom with underlying function verschiebungFun; it shifts coefficients up by one with a 0 at the start.
Русский
verschiebung — это гомоморфизм аддитивных моноидов с базовой функцией verschiebungFun; он сдвигает коэффициенты на одну позицию вверх, добавляя 0 в начале.
LaTeX
$$$$ \\text{verschiebung}: 𝕎R \\to 𝕎R, \\; \\text{toFun} = \\text{verschiebungFun}, \\; \\text{map_zero}'(x) = x, \\; \\text{map_add}'(x,y) = \\text{verschiebungFun}(x) + \\text{verschiebungFun}(y). $$$$
Lean4
/-- `verschiebung x` shifts the coefficients of `x` up by one, by inserting 0 as the 0th coefficient.
`x.coeff i` then becomes `(verschiebung x).coeff (i + 1)`.
This is an additive monoid hom with underlying function `verschiebung_fun`.
-/
noncomputable def verschiebung : 𝕎 R →+ 𝕎 R where
toFun := verschiebungFun
map_zero' := by ext ⟨⟩ <;> rw [verschiebungFun_coeff] <;> simp only [zero_coeff, ite_self]
map_add' := by
ghost_calc _ _
rintro ⟨⟩ <;> ghost_simp
