instDivisionCommMonoid — Mathlib

English

If G and H are DivisionCommMonoid, then G × H is a DivisionCommMonoid; multiplication commutes coordinatewise.

Русский

Если G и H — DivisionCommMonoid, то G × H — DivisionCommMonoid; умножение коммутативно по компонентам.

LaTeX

$$[DivisionCommMonoid G] [DivisionCommMonoid H] ⇒ DivisionCommMonoid (G × H) with (g1,h1)(g2,h2)=(g1g2,h1h2) and commutativity$$

Lean4

@[to_additive SubtractionCommMonoid]
instance [DivisionCommMonoid G] [DivisionCommMonoid H] : DivisionCommMonoid (G × H) :=
  { mul_comm := fun ⟨g₁, h₁⟩ ⟨_, _⟩ => by rw [mk_mul_mk, mul_comm g₁, mul_comm h₁]; rfl }

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