English
There is a natural multiplicative isomorphism between the units of a product and the product of units: (M × N)ˣ ≃* Mˣ × Nˣ.
Русский
Существует естественный мультипликативный изоморфизм между единицами произведения и произведением единиц: (M × N)ˣ ≃* Mˣ × Nˣ.
LaTeX
$$$ (\\mathrm{Units}(M \\times N))^{\\times} \\cong_* (\\mathrm{Units}(M)) \\times (\\mathrm{Units}(N)) $$$
Lean4
/-- The monoid equivalence between units of a product of two monoids, and the product of the
units of each monoid. -/
@[to_additive prodAddUnits /-- The additive monoid equivalence between additive units of a product
of two additive monoids, and the product of the additive units of each additive monoid. -/
]
def prodUnits : (M × N)ˣ ≃* Mˣ × Nˣ
where
toFun := (Units.map (MonoidHom.fst M N)).prod (Units.map (MonoidHom.snd M N))
invFun u := ⟨(u.1, u.2), (↑u.1⁻¹, ↑u.2⁻¹), by simp, by simp⟩
left_inv
u := by
simp only [MonoidHom.prod_apply, Units.coe_map, MonoidHom.coe_fst, MonoidHom.coe_snd, Prod.mk.eta,
Units.coe_map_inv, Units.mk_val]
right_inv := fun ⟨u₁, u₂⟩ =>
by
simp only [Units.map, MonoidHom.coe_fst, Units.inv_eq_val_inv, MonoidHom.coe_snd, MonoidHom.prod_apply,
Prod.mk.injEq]
exact ⟨rfl, rfl⟩
map_mul' := MonoidHom.map_mul _
