Mathlib v3 is deprecated. Go to Mathlib v4

Def monoid_hom.to_hom_units

Modification history

2022-01-05 23:45
src/algebra/group/units_hom.lean
chore(*): notation for `units` (#11236)
Modified monoid_hom.to_hom_unitsView on Github →
2020-05-12 06:37
src/algebra/group/units_hom.lean
feat(ring_theory/integral_domain): sum in integral domain indexed by finite group (#2623) …
Added monoid_hom.to_hom_unitsView on Github →