Commit 2026-02-15 13:39 63f4fac9

View on Github →

feat(Algebra/Group/Units/Hom): add map lemmas (#25993) This PR continues the work from #25609. Original PR: https://github.com/leanprover-community/mathlib4/pull/25609

Estimated changes

added theorem Units.val_inv_inj
added theorem IsUnit.unit_inv_map
added theorem IsUnit.unit_map
added theorem Units.map_bijective
modified theorem Units.map_injective
modified theorem Units.map_mk