Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 17:44 17da2776

View on Github →

feat(group_theory/eckmann_hilton): add Eckmann-Hilton (#335)

Estimated changes

Created group_theory/eckmann_hilton.lean

added def eckmann_hilton.comm_group

added def eckmann_hilton.comm_monoid

added theorem eckmann_hilton.group.is_unital

added theorem eckmann_hilton.mul

added theorem eckmann_hilton.mul_assoc

added theorem eckmann_hilton.mul_comm

added theorem eckmann_hilton.one