mathlib documentation

group_theory.eckmann_hilton

source
@[class]
structure eckmann_hilton.is_unital {X : Type u} (m : X → X → X) (e : X) :
Prop
  • one_mul : ∀ (x : X), m e x = x
  • mul_one : ∀ (x : X), m x e = x

source
theorem eckmann_hilton.group.is_unital {X : Type u} [G : group X] :
eckmann_hilton.is_unital has_mul.mul 1

source
theorem eckmann_hilton.one {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
e₁ = e₂

source
theorem eckmann_hilton.mul {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
m₁ = m₂

source
theorem eckmann_hilton.mul_comm {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
is_commutative X m₂

source
theorem eckmann_hilton.mul_assoc {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
is_associative X m₂

source
def eckmann_hilton.comm_monoid {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) (distrib : ∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) :
comm_monoid X

Equations
source
def eckmann_hilton.comm_group {X : Type u} {m₁ m₂ : X → X → X} {e₁ e₂ : X} (h₁ : eckmann_hilton.is_unital m₁ e₁) (h₂ : eckmann_hilton.is_unital m₂ e₂) [G : group X] (distrib : ∀ (a b c d : X), m₁ (a * b) (c * d) = (m₁ a c) * m₁ b d) :
comm_group X

Equations