English
There is an injection from NormalWord to PushoutI, via the product map; the map prod is injective.
Русский
Существует вложение из NormalWord в PushoutI через отображение произведения; prod инъективно.
LaTeX
$$$$\\text{prod} : \\mathrm{NormalWord}\, d \\to \\mathrm{PushoutI}(\\phi) \\text{ is injective}.$$$
Lean4
theorem cons_eq_smul {i : ι} (g : G i) (w : NormalWord d) (hmw : w.fstIdx ≠ some i) (hgr : g ∉ (φ i).range) :
cons g w hmw hgr = of (φ := φ) i g • w := by
apply ext_smul i
simp only [cons, Word.cons_eq_smul, MonoidHom.apply_ofInjective_symm, equiv_fst_eq_mul_inv, mul_assoc, map_mul,
map_inv, mul_smul, inv_smul_smul, summand_smul_def, equivPair, rcons, Word.equivPair_symm, Word.rcons_eq_smul,
Equiv.coe_fn_mk, Word.equivPair_tail_eq_inv_smul, Equiv.coe_fn_symm_mk, smul_inv_smul]
