instDivisionMonoid — Mathlib

English

If M and N are monoids, then M × N is a monoid with coordinatewise multiplication and identity.

Русский

Если M и N — моноиды, то M × N — моноид с по компонентам умножением и единицей.

LaTeX

$$$\text{Monoid}(M) \land \text{Monoid}(N) \Rightarrow \text{Monoid}(M \times N)$ with $(a,b)\cdot(c,d)=(ac,bd)$ and $1=(1_M,1_N)$$$

Lean4

@[to_additive]
instance [DivisionMonoid G] [DivisionMonoid H] : DivisionMonoid (G × H) :=
  { mul_inv_rev := fun _ _ => Prod.ext (mul_inv_rev _ _) (mul_inv_rev _ _),
    inv_eq_of_mul := fun _ _ h =>
      Prod.ext (inv_eq_of_mul_eq_one_right <| congr_arg fst h) (inv_eq_of_mul_eq_one_right <| congr_arg snd h),
    inv_inv := by simp }

Похожие утверждения