Def WithOne.unone

Modification history

2024-02-06 15:01

Mathlib/Algebra/Group/WithOne/Defs.lean

chore: Make sure `WithOne` doesn't import rings (#10275) …

Modified WithOne.unone View on Github →

2022-12-06 03:48

Mathlib/Algebra/Group/WithOne/Defs.lean

feat: port Algebra.Group.WithOne.Defs (#841) …

Added WithOne.unone View on Github →