Theorem Units.map_injective

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_injectiveView on Github →
2023-12-30 19:16
Mathlib/Algebra/Group/Units/Hom.lean
feat: Kummer extensions are cyclic. (#9119)
Added Units.map_injectiveView on Github →