English
Coordinatewise DivInvMonoid structure: div equals mul_inv, inv is defined componentwise and zpow acts componentwise.
Русский
Структура DivInvMonoid в произведении: деление равно умножению на обратное, обратное задается по компонентам, zpow действует по компонентам.
LaTeX
$$[DivInvMonoid G] [DivInvMonoid H] ⇒ (G × H) is DivInvMonoid with (g,h) / (g',h') = (g/g', h/h') and zpow defined componentwise$$
Lean4
@[to_additive Prod.subNegMonoid]
instance [DivInvMonoid G] [DivInvMonoid H] : DivInvMonoid (G × H)
where
div_eq_mul_inv _ _ := by ext <;> exact div_eq_mul_inv ..
zpow z a := ⟨DivInvMonoid.zpow z a.1, DivInvMonoid.zpow z a.2⟩
zpow_zero' _ := by ext <;> exact DivInvMonoid.zpow_zero' _
zpow_succ' _ _ := by ext <;> exact DivInvMonoid.zpow_succ' ..
zpow_neg' _ _ := by ext <;> exact DivInvMonoid.zpow_neg' ..
