prod_cons — Mathlib

English

The prod of the cons-constructed word equals the product of the base’s image and the new element.

Русский

Произведение конструированного слова через cons равно произведению образа основания на новый элемент.

LaTeX

$$$ (\mathrm{cons}\ g\ w\ hmw hgr).\mathrm{prod} = \mathrm{of}(i) g \cdot w.\mathrm{prod} $$$

Lean4

@[simp]
theorem prod_cons {i} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) :
    (cons g w hmw hgr).prod = of i g * w.prod := by
  simp [prod, cons, ← of_apply_eq_base φ i, equiv_fst_eq_mul_inv, mul_assoc]

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