Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โCtrl+โto navigate, Ctrl+๐ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl.
```/-
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin, Kenny Lau, Robert Y. Lewis

! This file was ported from Lean 3 source module group_theory.eckmann_hilton
! leanprover-community/mathlib commit 41cf0cc2f528dd40a8f2db167ea4fb37b8fde7f3
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs

/-!
# Eckmann-Hilton argument

The Eckmann-Hilton argument says that if a type carries two monoid structures that distribute
over one another, then they are equal, and in addition commutative.
The main application lies in proving that higher homotopy groups (`ฯโ` for `n โฅ 2`) are commutative.

## Main declarations

* `EckmannHilton.commMonoid`: If a type carries a unital magma structure that distributes
over a unital binary operation, then the magma is a commutative monoid.
* `EckmannHilton.commGroup`: If a type carries a group structure that distributes
over a unital binary operation, then the group is commutative.

-/

universe u

namespace EckmannHilton

variable {X: Type uX : Type u: Type (u+1)Type u}

/-- Local notation for `m a b`. -/
local notation a: ?m.180a " <" m: ?m.173m:51 "> " b: ?m.164b => m: ?m.173m a: ?m.180a b: ?m.164b

/-- `IsUnital m e` expresses that `e : X` is a left and right unit
for the binary operation `m : X โ X โ X`. -/
structure IsUnital: {X : Type u} โ (X โ X โ X) โ X โ PropIsUnital (m: X โ X โ Xm : X: Type uX โ X: Type uX โ X: Type uX) (e: Xe : X: Type uX) extends IsLeftId: (ฮฑ : Type ?u.1995) โ (ฮฑ โ ฮฑ โ ฮฑ) โ outParam ฮฑ โ PropIsLeftId _: Type ?u.1995_ m: X โ X โ Xm e: Xe, IsRightId: (ฮฑ : Type ?u.2006) โ (ฮฑ โ ฮฑ โ ฮฑ) โ outParam ฮฑ โ PropIsRightId _: Type ?u.2006_ m: X โ X โ Xm e: Xe : Prop: TypeProp
#align eckmann_hilton.is_unital EckmannHilton.IsUnital: {X : Type u} โ (X โ X โ X) โ X โ PropEckmannHilton.IsUnital

@[to_additive EckmannHilton.AddZeroClass.IsUnital: โ {X : Type u} [_G : AddZeroClass X], IsUnital (fun x x_1 => x + x_1) 0EckmannHilton.AddZeroClass.IsUnital]
theorem MulOneClass.isUnital: โ [_G : MulOneClass X], IsUnital (fun x x_1 => x * x_1) 1MulOneClass.isUnital [_G: MulOneClass X_G : MulOneClass: Type ?u.2027 โ Type ?u.2027MulOneClass X: Type uX] : IsUnital: {X : Type ?u.2030} โ (X โ X โ X) โ X โ PropIsUnital (ยท * ยท): X โ X โ X(ยท * ยท) (1: ?m.20681 : X: Type uX) :=
IsUnital.mk: โ {X : Type ?u.2209} {m : X โ X โ X} {e : X}, IsLeftId X m e โ IsRightId X m e โ IsUnital m eIsUnital.mk โจMulOneClass.one_mul: โ {M : Type ?u.2237} [self : MulOneClass M] (a : M), 1 * a = aMulOneClass.one_mulโฉ โจMulOneClass.mul_one: โ {M : Type ?u.2279} [self : MulOneClass M] (a : M), a * 1 = aMulOneClass.mul_oneโฉ
#align eckmann_hilton.mul_one_class.is_unital EckmannHilton.MulOneClass.isUnital: โ {X : Type u} [_G : MulOneClass X], IsUnital (fun x x_1 => x * x_1) 1EckmannHilton.MulOneClass.isUnital
#align eckmann_hilton.add_zero_class.is_unital EckmannHilton.AddZeroClass.IsUnital: โ {X : Type u} [_G : AddZeroClass X], IsUnital (fun x x_1 => x + x_1) 0EckmannHilton.AddZeroClass.IsUnital

variable {mโ: X โ X โ Xmโ mโ: X โ X โ Xmโ : X: Type uX โ X: Type uX โ X: Type uX} {eโ: Xeโ eโ: Xeโ : X: Type uX}

variable (hโ: IsUnital mโ eโhโ : IsUnital: {X : Type ?u.2341} โ (X โ X โ X) โ X โ PropIsUnital mโ: X โ X โ Xmโ eโ: Xeโ) (hโ: IsUnital mโ eโhโ : IsUnital: {X : Type ?u.2389} โ (X โ X โ X) โ X โ PropIsUnital mโ: X โ X โ Xmโ eโ: Xeโ)

variable (distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib : โ a: ?m.2400a b: ?m.3268b c: ?m.2461c d: ?m.2464d, ((a: ?m.2455a <mโ: X โ X โ Xmโ> b: ?m.2458b) <mโ: X โ X โ Xmโ> c: ?m.2461c <mโ: X โ X โ Xmโ> d: ?m.2464d) = (a: ?m.2400a <mโ: X โ X โ Xmโ> c: ?m.2461c) <mโ: X โ X โ Xmโ> b: ?m.2458b <mโ: X โ X โ Xmโ> d: ?m.2409d)

/-- If a type carries two unital binary operations that distribute over each other,
then they have the same unit elements.

In fact, the two operations are the same, and give a commutative monoid structure,
see `eckmann_hilton.CommMonoid`. -/
theorem one: โ {X : Type u} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ eโ = eโone : eโ: Xeโ = eโ: Xeโ := byGoals accomplished! ๐
X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)eโ = eโsimpa only [hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.2498} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.2527} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.2554} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.2583} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id] using distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib eโ: Xeโ eโ: Xeโ eโ: Xeโ eโ: XeโGoals accomplished! ๐
#align eckmann_hilton.one EckmannHilton.one: โ {X : Type u} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ eโ = eโEckmannHilton.one

/-- If a type carries two unital binary operations that distribute over each other,
then these operations are equal.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/
theorem mul: mโ = mโmul : mโ: X โ X โ Xmโ = mโ: X โ X โ Xmโ := byGoals accomplished! ๐
X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)mโ = mโfunext a: ?ฮฑa b: ?ฮฑbX: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xh.hmโ a b = mโ a b
X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)mโ = mโcalc
mโ: X โ X โ Xmโ a: ?ฮฑa b: ?ฮฑb = mโ: X โ X โ Xmโ (mโ: X โ X โ Xmโ a: ?ฮฑa eโ: Xeโ) (mโ: X โ X โ Xmโ eโ: Xeโ b: ?ฮฑb) := X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xh.hmโ a b = mโ a bbyGoals accomplished! ๐
X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xmโ a b = mโ (mโ a eโ) (mโ eโ b){X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xmโ a b = mโ (mโ a eโ) (mโ eโ b) X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xmโ a b = mโ (mโ a eโ) (mโ eโ b)simp only [one: โ {X : Type ?u.2880} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ eโ = eโone hโ: IsUnital mโ eโhโ hโ: IsUnital mโ eโhโ distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.2927} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.2956} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.2983} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.3012} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id]Goals accomplished! ๐ }Goals accomplished! ๐
_: ?mโ_ = mโ: X โ X โ Xmโ a: ?ฮฑa b: ?ฮฑb := X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xh.hmโ a b = mโ a bbyGoals accomplished! ๐ X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xmโ (mโ a eโ) (mโ eโ b) = mโ a bsimp only [distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.3085} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.3111} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.3137} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.3163} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id]Goals accomplished! ๐
#align eckmann_hilton.mul EckmannHilton.mul: โ {X : Type u} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ mโ = mโEckmannHilton.mul

/-- If a type carries two unital binary operations that distribute over each other,
then these operations are commutative.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/
theorem mul_comm: IsCommutative X mโmul_comm : IsCommutative: (ฮฑ : Type ?u.3281) โ (ฮฑ โ ฮฑ โ ฮฑ) โ PropIsCommutative _: Type ?u.3281_ mโ: X โ X โ Xmโ :=
โจfun a: ?m.3303a b: ?m.3306b => byGoals accomplished! ๐ X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b: Xmโ a b = mโ b asimpa [mul: โ {X : Type ?u.3318} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ mโ = mโmul hโ: IsUnital mโ eโhโ hโ: IsUnital mโ eโhโ distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.3362} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.3391} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id] using distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib eโ: Xeโ a: Xa b: Xb eโ: XeโGoals accomplished! ๐โฉ
#align eckmann_hilton.mul_comm EckmannHilton.mul_comm: โ {X : Type u} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ IsCommutative X mโEckmannHilton.mul_comm

/-- If a type carries two unital binary operations that distribute over each other,
then these operations are associative.

In fact, they give a commutative monoid structure, see `eckmann_hilton.CommMonoid`. -/
theorem mul_assoc: IsAssociative X mโmul_assoc : IsAssociative: (ฮฑ : Type ?u.3543) โ (ฮฑ โ ฮฑ โ ฮฑ) โ PropIsAssociative _: Type ?u.3543_ mโ: X โ X โ Xmโ :=
โจfun a: ?m.3565a b: ?m.3568b c: ?m.3571c => byGoals accomplished! ๐ X: Type umโ, mโ: X โ X โ Xeโ, eโ: Xhโ: IsUnital mโ eโhโ: IsUnital mโ eโdistrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)a, b, c: Xmโ (mโ a b) c = mโ a (mโ b c)simpa [mul: โ {X : Type ?u.3585} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ mโ = mโmul hโ: IsUnital mโ eโhโ hโ: IsUnital mโ eโhโ distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib, hโ: IsUnital mโ eโhโ.left_id: โ {ฮฑ : Type ?u.3629} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsLeftId ฮฑ op o] (a : ฮฑ), op o a = aleft_id, hโ: IsUnital mโ eโhโ.right_id: โ {ฮฑ : Type ?u.3658} {op : ฮฑ โ ฮฑ โ ฮฑ} {o : outParam ฮฑ} [self : IsRightId ฮฑ op o] (a : ฮฑ), op a o = aright_id] using distrib: โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)distrib a: Xa b: Xb eโ: Xeโ c: XcGoals accomplished! ๐โฉ
#align eckmann_hilton.mul_assoc EckmannHilton.mul_assoc: โ {X : Type u} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ IsAssociative X mโEckmannHilton.mul_assoc

/-- If a type carries a unital magma structure that distributes over a unital binary
operation, then the magma structure is a commutative monoid. -/
@[to_additive: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [h : AddZeroClass X] โ (โ (a b c d : X), mโ (a + b) (c + d) = mโ a c + mโ b d) โ AddCommMonoid Xto_additive (attr := reducible)
"If a type carries a unital additive magma structure that distributes over a unital binary
operation, then the additive magma structure is a commutative additive monoid."]
def commMonoid: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [h : MulOneClass X] โ (โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b d) โ CommMonoid XcommMonoid [h: MulOneClass Xh : MulOneClass: Type ?u.3809 โ Type ?u.3809MulOneClass X: Type uX]
(distrib: โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b ddistrib : โ a: ?m.3813a b: ?m.3816b c: ?m.3819c d: ?m.3822d, ((a: ?m.3813a * b: ?m.3816b) <mโ: X โ X โ Xmโ> c: ?m.3819c * d: ?m.3822d) = (a: ?m.3813a <mโ: X โ X โ Xmโ> c: ?m.3819c) * b: ?m.3816b <mโ: X โ X โ Xmโ> d: ?m.3822d) : CommMonoid: Type ?u.3928 โ Type ?u.3928CommMonoid X: Type uX :=
{ h: MulOneClass Xh with
mul := (ยท * ยท): X โ X โ X(ยท * ยท), one := 1: ?m.40601, mul_comm := (mul_comm: โ {X : Type ?u.4184} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ IsCommutative X mโmul_comm hโ: IsUnital mโ eโhโ MulOneClass.isUnital: โ {X : Type ?u.4197} [_G : MulOneClass X], IsUnital (fun x x_1 => x * x_1) 1MulOneClass.isUnital distrib: โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b ddistrib).comm: โ {ฮฑ : Type ?u.4219} {op : ฮฑ โ ฮฑ โ ฮฑ} [self : IsCommutative ฮฑ op] (a b : ฮฑ), op a b = op b acomm,
mul_assoc := (mul_assoc: โ {X : Type ?u.3989} {mโ mโ : X โ X โ X} {eโ eโ : X},
IsUnital mโ eโ โ IsUnital mโ eโ โ (โ (a b c d : X), mโ (mโ a b) (mโ c d) = mโ (mโ a c) (mโ b d)) โ IsAssociative X mโmul_assoc hโ: IsUnital mโ eโhโ MulOneClass.isUnital: โ {X : Type ?u.4007} [_G : MulOneClass X], IsUnital (fun x x_1 => x * x_1) 1MulOneClass.isUnital distrib: โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b ddistrib).assoc: โ {ฮฑ : Type ?u.4034} {op : ฮฑ โ ฮฑ โ ฮฑ} [self : IsAssociative ฮฑ op] (a b c : ฮฑ), op (op a b) c = op a (op b c)assoc }
#align eckmann_hilton.comm_monoid EckmannHilton.commMonoid: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [h : MulOneClass X] โ (โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b d) โ CommMonoid XEckmannHilton.commMonoid
#align eckmann_hilton.add_comm_monoid EckmannHilton.addCommMonoid: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [h : AddZeroClass X] โ (โ (a b c d : X), mโ (a + b) (c + d) = mโ a c + mโ b d) โ AddCommMonoid XEckmannHilton.addCommMonoid

/-- If a type carries a group structure that distributes over a unital binary operation,
then the group is commutative. -/
@[to_additive: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [G : AddGroup X] โ (โ (a b c d : X), mโ (a + b) (c + d) = mโ a c + mโ b d) โ AddCommGroup Xto_additive (attr := reducible)
"If a type carries an additive group structure that distributes over a unital binary
operation, then the additive group is commutative."]
def commGroup: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ IsUnital mโ eโ โ [G : Group X] โ (โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b d) โ CommGroup XcommGroup [G: Group XG : Group: Type ?u.4810 โ Type ?u.4810Group X: Type uX]
(distrib: โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b ddistrib : โ a: ?m.4814a b: ?m.4817b c: ?m.4820c d: ?m.4823d, ((a: ?m.4814a * b: ?m.4817b) <mโ: X โ X โ Xmโ> c: ?m.4820c * d: ?m.4823d) = (a: ?m.4814a <mโ: X โ X โ Xmโ> c: ?m.4820c) * b: ?m.4817b <mโ: X โ X โ Xmโ> d: ?m.4823d) : CommGroup: Type ?u.4991 โ Type ?u.4991CommGroup X: Type uX :=
{ EckmannHilton.commMonoid: {X : Type ?u.4997} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [h : MulOneClass X] โ (โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b d) โ CommMonoid XEckmannHilton.commMonoid hโ: IsUnital mโ eโhโ distrib: โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b ddistrib, G: Group XG with .. }
#align eckmann_hilton.comm_group EckmannHilton.commGroup: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ IsUnital mโ eโ โ [G : Group X] โ (โ (a b c d : X), mโ (a * b) (c * d) = mโ a c * mโ b d) โ CommGroup XEckmannHilton.commGroup
#align eckmann_hilton.add_comm_group EckmannHilton.addCommGroup: {X : Type u} โ
{mโ : X โ X โ X} โ
{eโ : X} โ
IsUnital mโ eโ โ [G : AddGroup X] โ (โ (a b c d : X), mโ (a + b) (c + d) = mโ a c + mโ b d) โ AddCommGroup XEckmannHilton.addCommGroup

end EckmannHilton
```