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.
```/-
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

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

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
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
{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