English
Equivalence demonstrating compatibility of Prod with Multiplicative structures under Opposite translations.
Русский
Эквиваленция, демонстрирующая совместимость произведения с умножительными структурами при противоположных переводах.
LaTeX
$$$\\text{MulEquiv}.prodMultiplicative\\,(G,H) : \\text{MulEquiv}(\\text{Multiplicative}(Prod\,G\,H)) (\\text{Prod}(\\text{Multiplicative}G, \\text{Multiplicative}H))$$$
Lean4
/-- `Multiplicative (G × H)` is equivalent to `Multiplicative G × Multiplicative H`. -/
@[simps]
def prodMultiplicative [Add G] [Add H] : Multiplicative (G × H) ≃* Multiplicative G × Multiplicative H
where
toFun x := (Multiplicative.ofAdd x.toAdd.1, Multiplicative.ofAdd x.toAdd.2)
invFun := fun (x, y) ↦ Multiplicative.ofAdd (x.toAdd, y.toAdd)
map_mul' _ _ := rfl
