English
If G and H are DivInvMonoid, then G × H is a DivInvMonoid with operations defined coordinatewise; in particular, div equals mul inverse and zpow acts componentwise.
Русский
Если G и H — DivInvMonoid, то G × H — DivInvMonoid; деление равно умножению на обратное и zpow действует по компонентам.
LaTeX
$$$ (g,h) / (g',h') = (g/g',\, h/h') \\,;\\; (g,h)^{-z} = (g^{-z}, h^{-z}) $$$
Lean4
@[to_additive]
instance instMonoid [Monoid M] [Monoid N] : Monoid (M × N) :=
{ npow := fun z a => ⟨Monoid.npow z a.1, Monoid.npow z a.2⟩,
npow_zero := fun _ => Prod.ext (Monoid.npow_zero _) (Monoid.npow_zero _),
npow_succ := fun _ _ => Prod.ext (Monoid.npow_succ _ _) (Monoid.npow_succ _ _), one_mul := by simp,
mul_one := by simp }
