@[class]
theorem
eckmann_hilton.one
{X : Type u}
{m₁ m₂ : X → X → X}
{e₁ e₂ : X} :
eckmann_hilton.is_unital m₁ e₁ → eckmann_hilton.is_unital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → e₁ = e₂
theorem
eckmann_hilton.mul
{X : Type u}
{m₁ m₂ : X → X → X}
{e₁ e₂ : X} :
eckmann_hilton.is_unital m₁ e₁ → eckmann_hilton.is_unital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → m₁ = m₂
theorem
eckmann_hilton.mul_comm
{X : Type u}
{m₁ m₂ : X → X → X}
{e₁ e₂ : X} :
eckmann_hilton.is_unital m₁ e₁ → eckmann_hilton.is_unital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → is_commutative X m₂
theorem
eckmann_hilton.mul_assoc
{X : Type u}
{m₁ m₂ : X → X → X}
{e₁ e₂ : X} :
eckmann_hilton.is_unital m₁ e₁ → eckmann_hilton.is_unital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → is_associative X m₂
def
eckmann_hilton.comm_monoid
{X : Type u}
{m₁ m₂ : X → X → X}
{e₁ e₂ : X} :
eckmann_hilton.is_unital m₁ e₁ → eckmann_hilton.is_unital m₂ e₂ → (∀ (a b c d : X), m₁ (m₂ a b) (m₂ c d) = m₂ (m₁ a c) (m₁ b d)) → comm_monoid X
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] :
(∀ (a b c d : X), m₁ (a * b) (c * d) = m₁ a c * m₁ b d) → comm_group X