Theorem Units.map_mk

Modification history

2026-02-15 13:39

Mathlib/Algebra/Group/Units/Hom.lean

feat(Algebra/Group/Units/Hom): add map lemmas (#25993) …

Modified Units.map_mk View on Github →

2024-12-10 15:41

Mathlib/Algebra/Group/Units/Hom.lean

feat: `Units.map` of `Units.mk` (#19867) …

Added Units.map_mk View on Github →