commMonoidOfExponentTwo — Mathlib

English

There exists a commutative monoid structure on a set G given exponent G = 2.

Русский

Существует коммутативная структура моноида на множестве G при условии exp(G)=2.

LaTeX

$$$\text{commMonoidOfExponentTwo }(G) : \text{CommMonoid } G\text{ given } \operatorname{exponent} G = 2$$$

Lean4

/-- Any cancellative monoid of exponent two is abelian. -/
@[to_additive /-- Any additive group of exponent two is abelian. -/
    ]
abbrev commMonoidOfExponentTwo [IsCancelMul G] (hG : Monoid.exponent G = 2) : CommMonoid G where
  mul_comm := mul_comm_of_exponent_two hG

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