prod_smul — Mathlib

English

Alternative statement of prod injectivity in the pushout context: the map prod is injective when considered as a map from NormalWord d to PushoutI φ.

Русский

Альтернативное утверждение инъективности prod в контексте пушаута: prod инъективно как отображение из NormalWord d в PushoutI φ.

LaTeX

$$$$\\text{prod} : \\mathrm{NormalWord}\, d \\to \\mathrm{PushoutI}(\\phi) \\text{ injective}.$$$$

Lean4

@[simp]
theorem prod_smul (g : PushoutI φ) (w : NormalWord d) : (g • w).prod = g * w.prod := by
  induction g using PushoutI.induction_on generalizing w with
  | of i g => rw [of_smul_eq_smul, prod_summand_smul]
  | base h => rw [base_smul_eq_smul, prod_base_smul]
  | mul x y ihx ihy => rw [mul_smul, ihx, ihy, mul_assoc]

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