Mathlib v3 is deprecated. Go to Mathlib v4

Theorem monoid_hom.coe_to_hom_units

Modification history

2022-11-25 02:14
src/algebra/hom/units.lean
feat(group_theory/subgroup/basic): weaken some TC assumptions (#17698) …
Modified monoid_hom.coe_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.coe_to_hom_unitsView on Github →