Commit 2023-08-07 13:57 9a63798c

View on Github →

feat(Group): constructors for minimal group axioms (#6173)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Defs.lean

Created Mathlib/Algebra/Group/MinimalAxioms.lean

added def Group.ofLeftAxioms

added def Group.ofRightAxioms