Commit 2022-11-23 19:23 8b2d8445

View on Github →

feat: port Algebra.GroupTheory.EckmannHilton (#626) mathlib3 sha: 71dbd401af609bb5065d060b8f221d2a31e2b8d7

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/EckmannHilton.lean

added structure EckmannHilton.IsUnital

added theorem EckmannHilton.MulOneClass.isUnital

added def EckmannHilton.commGroup

added def EckmannHilton.commMonoid

added theorem EckmannHilton.mul

added theorem EckmannHilton.mul_assoc

added theorem EckmannHilton.mul_comm

added theorem EckmannHilton.one