summandAction — Mathlib

English

The action smul is exactly the rcons construction updating the head by multiplication with the old head.

Русский

Действие smul равно преобразованию rcons, где голова обновляется умножением на прежнюю голову.

LaTeX

$$$$ m \\cdot w = \\mathrm{rcons}\\{ \\operatorname{equivPair}(i,w) with head := m \\cdot (\\operatorname{equivPair}(i,w)).head \\} $$$$

Lean4

instance summandAction (i) : MulAction (M i) (Word M)
    where
  smul m w := rcons { equivPair i w with head := m * (equivPair i w).head }
  one_smul
    w := by
    apply (equivPair i).symm_apply_eq.mpr
    simp [equivPair]
  mul_smul m m'
    w := by
    dsimp [instHSMul]
    simp [mul_assoc, ← equivPair_symm, Equiv.apply_symm_apply]

Похожие утверждения