Mathlib v3 is deprecated. Go to Mathlib v4

Theorem is_unit.map'

Modification history

2021-08-01 17:17
src/deprecated/group.lean
chore(deprecated/*): Make deprecated classes into structures (#8178) …
Modified is_unit.map'View on Github →
2020-03-02 14:25
src/algebra/group/is_unit.lean
chore(algebra/group): move `is_mul/monoid/group_hom` to `deprecated/` (#2056) …
Modified is_unit.map'View on Github →
2020-02-19 11:05
src/algebra/associated.lean
refactor(algebra/associated): move `is_unit` def to `algebra/group` (#2015) …
Modified is_unit.map'View on Github →
2019-08-15 05:08
src/algebra/associated.lean
chore(*): migrate `units.map` to bundled homs (#1331)
Added is_unit.map'View on Github →