toHomUnits_mul — Mathlib

English

The map sending a homomorphism f to f.toHomUnits preserves multiplication: (f g)^{toHomUnits} = f^{toHomUnits} · g^{toHomUnits}.

Русский

Отображение гомоморфизмов через toHomUnits сохраняет произведение: (f g)^{toHomUnits} = f^{toHomUnits} · g^{toHomUnits}.

LaTeX

$$$(f \\ast g)^{\\mathrm{toHomUnits}} = f^{\\mathrm{toHomUnits}} \\cdot g^{\\mathrm{toHomUnits}},$$$

Lean4

@[simp]
theorem toHomUnits_mul (f g : G →* M) : (f * g).toHomUnits = f.toHomUnits * g.toHomUnits := by ext; rfl

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