English
An isomorphism AddEquiv on the additive side corresponds to a multiplicative isomorphism on the product side; the additive product corresponds to product of additives.
Русский
Изоморфизм AddEquiv на аддитивной стороне соответствует множительному изоморфизму на произведении; аддитивное произведение соответствует произведению аддитивных.
LaTeX
$$$\\text{AddEquiv}(G,H) \\simeq \\text{MulEquiv}(\\text{Multiplicative } G) (\\text{Multiplicative } H)$$$
Lean4
/-- `Additive (G × H)` is equivalent to `Additive G × Additive H`. -/
@[simps]
def prodAdditive [Mul G] [Mul H] : Additive (G × H) ≃+ Additive G × Additive H
where
toFun x := (Additive.ofMul x.toMul.1, Additive.ofMul x.toMul.2)
invFun := fun (x, y) ↦ Additive.ofMul (x.toMul, y.toMul)
map_add' _ _ := rfl
