English
Let (M_i) be a family of monoids indexed by i. Then the units of the product monoid ∏_i M_i are canonically isomorphic to the product of the units of each factor: (∏_i M_i)ˣ ≅ ∏_i (M_i)ˣ.
Русский
Пусть (M_i) — семейство моноидов, индексируемое i. Тогда области единиц произведения моноидов ∏_i M_i естественным образом изоморфны произведению единиц каждого множителя: (∏_i M_i)ˣ ≅ ∏_i (M_i)ˣ.
LaTeX
$$$(\prod_{i} M_i)^{\times} \cong \prod_{i} M_i^{\times}$$$
Lean4
/-- The monoid equivalence between units of a product,
and the product of the units of each monoid. -/
@[to_additive (attr := simps) /-- The additive-monoid equivalence between (additive) units of a product,
and the product of the (additive) units of each monoid. -/
]
def piUnits : (Π i, M i)ˣ ≃* Π i, (M i)ˣ
where
toFun f i := ⟨f.val i, f.inv i, congr_fun f.val_inv i, congr_fun f.inv_val i⟩
invFun f := ⟨(val <| f ·), (inv <| f ·), funext (val_inv <| f ·), funext (inv_val <| f ·)⟩
map_mul' _ _ := rfl
