/-
Copyright (c) 2018 Kenny Lau. All rights reserved.
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 u
X : 
Type u: Type (u+1)
Type u}

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

/-- `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 → Prop
IsUnital (
m: X → X → X
m : 
X: Type u
X → 
X: Type u
X → 
X: Type u
X) (
e: X
e : 
X: Type u
X) extends 
IsLeftId: (α : Type ?u.1995) → (α → α → α) → outParam α → Prop
IsLeftId 
_: Type ?u.1995
_ 
m: X → X → X
m 
e: X
e, 
IsRightId: (α : Type ?u.2006) → (α → α → α) → outParam α → Prop
IsRightId 
_: Type ?u.2006
_ 
m: X → X → X
m 
e: X
e : 
Prop: Type
Prop
#align eckmann_hilton.is_unital 
EckmannHilton.IsUnital: {X : Type u} → (X → X → X) → X → Prop
EckmannHilton.IsUnital

@[to_additive 
EckmannHilton.AddZeroClass.IsUnital: ∀ {X : Type u} [_G : AddZeroClass X], IsUnital (fun x x_1 => x + x_1) 0
EckmannHilton.AddZeroClass.IsUnital]
theorem 
MulOneClass.isUnital: ∀ [_G : MulOneClass X], IsUnital (fun x x_1 => x * x_1) 1
MulOneClass.isUnital [
_G: MulOneClass X
_G : 
MulOneClass: Type ?u.2027 → Type ?u.2027
MulOneClass 
X: Type u
X] : 
IsUnital: {X : Type ?u.2030} → (X → X → X) → X → Prop
IsUnital 
(· * ·): X → X → X
(· * ·) (
1: ?m.2068
1 : 
X: Type u
X) :=
  
IsUnital.mk: ∀ {X : Type ?u.2209} {m : X → X → X} {e : X}, IsLeftId X m e → IsRightId X m e → IsUnital m e
IsUnital.mk ⟨
MulOneClass.one_mul: ∀ {M : Type ?u.2237} [self : MulOneClass M] (a : M), 1 * a = a
MulOneClass.one_mul⟩ ⟨
MulOneClass.mul_one: ∀ {M : Type ?u.2279} [self : MulOneClass M] (a : M), a * 1 = a
MulOneClass.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) 1
EckmannHilton.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) 0
EckmannHilton.AddZeroClass.IsUnital

variable {
m₁: X → X → X
m₁ 
m₂: X → X → X
m₂ : 
X: Type u
X → 
X: Type u
X → 
X: Type u
X} {
e₁: X
e₁ 
e₂: X
e₂ : 
X: Type u
X}

variable (
h₁: IsUnital m₁ e₁
h₁ : 
IsUnital: {X : Type ?u.2341} → (X → X → X) → X → Prop
IsUnital 
m₁: X → X → X
m₁ 
e₁: X
e₁) (
h₂: IsUnital m₂ e₂
h₂ : 
IsUnital: {X : Type ?u.2389} → (X → X → X) → X → Prop
IsUnital 
m₂: X → X → X
m₂ 
e₂: X
e₂)

variable (
distrib: ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
distrib : ∀ 
a: ?m.2400
a 
b: ?m.3268
b 
c: ?m.2461
c 
d: ?m.2464
d, ((
a: ?m.2455
a <
m₂: X → X → X
m₂> 
b: ?m.2458
b) <
m₁: X → X → X
m₁> 
c: ?m.2461
c <
m₂: X → X → X
m₂> 
d: ?m.2464
d) = (
a: ?m.2400
a <
m₁: X → X → X
m₁> 
c: ?m.2461
c) <
m₂: X → X → X
m₂> 
b: ?m.2458
b <
m₁: X → X → X
m₁> 
d: ?m.2409
d)

/-- 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₁: X
e₁ = 
e₂: X
e₂ := by
Goals accomplished! 🐙
  
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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 = a
left_id, 
h₁: IsUnital m₁ e₁
h₁.
right_id: ∀ {α : Type ?u.2527} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id, 
h₂: IsUnital m₂ e₂
h₂.
left_id: ∀ {α : Type ?u.2554} {op : α → α → α} {o : outParam α} [self : IsLeftId α op o] (a : α), op o a = a
left_id, 
h₂: IsUnital m₂ e₂
h₂.
right_id: ∀ {α : Type ?u.2583} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id] using 
distrib: ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
distrib 
e₂: X
e₂ 
e₁: X
e₁ 
e₁: X
e₁ 
e₂: X
e₂
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 → X
m₁ = 
m₂: X → X → X
m₂ := by
Goals accomplished! 🐙
  
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: ?α
b
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

h.h
m₁ a b = m₂ a b
  
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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 → X
m₁ 
a: ?α
a 
b: ?α
b = 
m₁: X → X → X
m₁ (
m₂: X → X → X
m₂ 
a: ?α
a 
e₁: X
e₁) (
m₂: X → X → X
m₂ 
e₁: X
e₁ 
b: ?α
b) := 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

h.h
m₁ a b = m₂ a bby
Goals accomplished! 🐙
      
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b){
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₁ a b = m₁ (m₂ a e₁) (m₂ e₁ b) 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₁ 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 = a
left_id, 
h₁: IsUnital m₁ e₁
h₁.
right_id: ∀ {α : Type ?u.2956} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id, 
h₂: IsUnital m₂ e₂
h₂.
left_id: ∀ {α : Type ?u.2983} {op : α → α → α} {o : outParam α} [self : IsLeftId α op o] (a : α), op o a = a
left_id, 
h₂: IsUnital m₂ e₂
h₂.
right_id: ∀ {α : Type ?u.3012} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id]
Goals accomplished! 🐙 }
Goals accomplished! 🐙
    
_: ?m✝
_ = 
m₂: X → X → X
m₂ 
a: ?α
a 
b: ?α
b := 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

h.h
m₁ a b = m₂ a bby
Goals accomplished! 🐙 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₁ (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 = a
left_id, 
h₁: IsUnital m₁ e₁
h₁.
right_id: ∀ {α : Type ?u.3111} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id, 
h₂: IsUnital m₂ e₂
h₂.
left_id: ∀ {α : Type ?u.3137} {op : α → α → α} {o : outParam α} [self : IsLeftId α op o] (a : α), op o a = a
left_id, 
h₂: IsUnital m₂ e₂
h₂.
right_id: ∀ {α : Type ?u.3163} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_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) → (α → α → α) → Prop
IsCommutative 
_: Type ?u.3281
_ 
m₂: X → X → X
m₂ :=
  ⟨fun 
a: ?m.3303
a 
b: ?m.3306
b => by
Goals accomplished! 🐙 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₂ 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 = a
left_id, 
h₂: IsUnital m₂ e₂
h₂.
right_id: ∀ {α : Type ?u.3391} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id] using 
distrib: ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
distrib 
e₂: X
e₂ 
a: X
a 
b: X
b 
e₂: X
e₂
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) → (α → α → α) → Prop
IsAssociative 
_: Type ?u.3543
_ 
m₂: X → X → X
m₂ :=
  ⟨fun 
a: ?m.3565
a 
b: ?m.3568
b 
c: ?m.3571
c => by
Goals accomplished! 🐙 
X: Type u

m₁, m₂: X → X → X

e₁, e₂: X

h₁: 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: X

m₂ (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 = a
left_id, 
h₂: IsUnital m₂ e₂
h₂.
right_id: ∀ {α : Type ?u.3658} {op : α → α → α} {o : outParam α} [self : IsRightId α op o] (a : α), op a o = a
right_id] using 
distrib: ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)
distrib 
a: X
a 
b: X
b 
e₂: X
e₂ 
c: X
c
Goals 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 X
to_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 X
commMonoid [
h: MulOneClass X
h : 
MulOneClass: Type ?u.3809 → Type ?u.3809
MulOneClass 
X: Type u
X]
    (
distrib: ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d
distrib : ∀ 
a: ?m.3813
a 
b: ?m.3816
b 
c: ?m.3819
c 
d: ?m.3822
d, ((
a: ?m.3813
a * 
b: ?m.3816
b) <
m₁: X → X → X
m₁> 
c: ?m.3819
c * 
d: ?m.3822
d) = (
a: ?m.3813
a <
m₁: X → X → X
m₁> 
c: ?m.3819
c) * 
b: ?m.3816
b <
m₁: X → X → X
m₁> 
d: ?m.3822
d) : 
CommMonoid: Type ?u.3928 → Type ?u.3928
CommMonoid 
X: Type u
X :=
  { 
h: MulOneClass X
h with
      mul := 
(· * ·): X → X → X
(· * ·), one := 
1: ?m.4060
1, 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) 1
MulOneClass.isUnital 
distrib: ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d
distrib).
comm: ∀ {α : Type ?u.4219} {op : α → α → α} [self : IsCommutative α op] (a b : α), op a b = op b a
comm,
      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) 1
MulOneClass.isUnital 
distrib: ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d
distrib).
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 X
EckmannHilton.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 X
EckmannHilton.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 X
to_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 X
commGroup [
G: Group X
G : 
Group: Type ?u.4810 → Type ?u.4810
Group 
X: Type u
X]
    (
distrib: ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d
distrib : ∀ 
a: ?m.4814
a 
b: ?m.4817
b 
c: ?m.4820
c 
d: ?m.4823
d, ((
a: ?m.4814
a * 
b: ?m.4817
b) <
m₁: X → X → X
m₁> 
c: ?m.4820
c * 
d: ?m.4823
d) = (
a: ?m.4814
a <
m₁: X → X → X
m₁> 
c: ?m.4820
c) * 
b: ?m.4817
b <
m₁: X → X → X
m₁> 
d: ?m.4823
d) : 
CommGroup: Type ?u.4991 → Type ?u.4991
CommGroup 
X: Type u
X :=
  { 
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 X
EckmannHilton.commMonoid 
h₁: IsUnital m₁ e₁
h₁ 
distrib: ∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d
distrib, 
G: Group X
G 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 X
EckmannHilton.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 X
EckmannHilton.addCommGroup

end EckmannHilton