Def Group.ofLeftAxioms

Modification history

2024-08-09 14:59
Mathlib/Algebra/Group/MinimalAxioms.lean
perf: `to_additive (attr := reducible)` -> `abbrev` (#15476)
Deleted Group.ofLeftAxiomsView on Github →
2023-08-07 13:57
Mathlib/Algebra/Group/MinimalAxioms.lean
feat(Group): constructors for minimal group axioms (#6173)
Added Group.ofLeftAxiomsView on Github →