Def Units.map'

Modification history

2024-05-07 01:05
Mathlib/Deprecated/Group.lean
refactor: replace `@[reducible]` with `abbrev` (#12614) …
Deleted Units.map'View on Github →
2023-01-06 08:41
Mathlib/Deprecated/Group.lean
feat: Port `Deprecated.Group` and `Deprecated.Ring` (#1368)
Added Units.map'View on Github →