English
If a type carries a group structure that distributes over a unital binary operation, then the underlying group is commutative.
Русский
Если множество со структурой группы дистрибутивно распределяется над единичной бинарной операцией, то группа коммутативна.
LaTeX
$$$\\forall a,b\\in X,\\ a\\cdot b = b\\cdot a$$$
Lean4
/-- If a type carries a group structure that distributes over a unital binary operation,
then the group is commutative. -/
@[to_additive /-- If a type carries an additive group structure that distributes over a unital binary
operation, then the additive group is commutative. -/
]
abbrev commGroup [G : Group X] (distrib : ∀ a b c d, ((a * b) <m₁> c * d) = (a <m₁> c) * b <m₁> d) : CommGroup X :=
{ EckmannHilton.commMonoid h₁ distrib, G with .. }
