English
For χ1, χ2 : MulChar R R' and a ∈ R^×, the unit-homomorphism of the product equals the product of unit-homomorphisms: equivToUnitHom(χ1 · χ2)(a) = equivToUnitHom(χ1)(a) · equivToUnitHom(χ2)(a).
Русский
Для χ1, χ2 : MulChar R R' и элемента a из R^×, единично-оморфизм произведения равен произведению единично-оморфизмов: equivToUnitHom(χ1 · χ2)(a) = equivToUnitHom(χ1)(a) · equivToUnitHom(χ2)(a).
LaTeX
$$$$ \\mathrm{equivToUnitHom}(\\chi_1 \\ast \\chi_2)(a) = \\mathrm{equivToUnitHom}(\\chi_1)(a) \\cdot \\mathrm{equivToUnitHom}(\\chi_2)(a). $$$$
Lean4
theorem equivToUnitHom_mul_apply (χ₁ χ₂ : MulChar R R') (a : Rˣ) :
equivToUnitHom (χ₁ * χ₂) a = equivToUnitHom χ₁ a * equivToUnitHom χ₂ a :=
by
apply_fun ((↑) : R'ˣ → R') using Units.val_injective
push_cast
simp_rw [coe_equivToUnitHom, coeToFun_mul, Pi.mul_apply]
