prod_smul — Mathlib

English

The product map respects smul: prod(m • w) = m · prod(w).

Русский

Производственная карта сохраняет smul: prod(m • w) = m · prod(w).

LaTeX

$$$$ prod( m \\cdot w ) = m \\cdot prod(w) $$$$

Lean4

@[simp]
theorem prod_smul (m) : ∀ w : Word M, prod (m • w) = m * prod w := by
  induction m using CoprodI.induction_on with
  | one =>
    intro
    rw [one_smul, one_mul]
  | of _ =>
    intros
    rw [of_smul_def, prod_rcons, of.map_mul, mul_assoc, ← prod_rcons, ← equivPair_symm, Equiv.symm_apply_apply]
  | mul x y hx hy =>
    intro w
    rw [mul_smul, hx, hy, mul_assoc]

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