equivPair_smul_same — Mathlib

English

The equivalence pair after smul by m in the i-component equals head multiplied by m, tail unchanged.

Русский

Пара эквививалентности после умножения на m в i-компоненте имеет голову, равную умножению головы на m, хвост сохраняется.

LaTeX

$$$$ equivPair(i, \\mathrm{of} m \\cdot w) = \\langle m \\cdot (equivPair(i,w)).head, (equivPair(i,w)).tail, (equivPair(i,w)).fstIdx\\_ne \\rangle $$$$

Lean4

theorem equivPair_smul_same {i} (m : M i) (w : Word M) :
    equivPair i (of m • w) = ⟨m * (equivPair i w).head, (equivPair i w).tail, (equivPair i w).fstIdx_ne⟩ :=
  by
  rw [of_smul_def, ← equivPair_symm]
  simp

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