Commit 2022-12-03 03:40 1078125d

View on Github →

feat: port Algebra.Hom.Units (#745) mathlib3 SHA: 76171581280d5b5d1e2d1f4f37e5420357bdc636 Seems relatively straightforward. Some lemma names (e.g. units.coe_zpow -> Units.val_zpow_eq_zpow_val) are renamed to refer to val instead of coe, following the convention used in Algebra.Group.Units.

depends on: #659

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Hom/Group.lean

Created Mathlib/Algebra/Hom/Units.lean

added theorem Group.isUnit

added theorem IsUnit.coe_liftRight

added theorem IsUnit.div

added theorem IsUnit.eq_on_inv

added theorem IsUnit.inv

added theorem IsUnit.liftRight_inv_mul

added theorem IsUnit.map

added theorem IsUnit.mul_liftRight_inv

added theorem IsUnit.of_leftInverse

added def IsUnit.unit'

added theorem MonoidHom.coe_toHomUnits

added def MonoidHom.toHomUnits

added def Units.coeHom

added theorem Units.coeHom_apply

added theorem Units.coe_liftRight

added theorem Units.coe_map

added theorem Units.coe_map_inv

added def Units.liftRight

added theorem Units.liftRight_inv_mul

added def Units.map

added theorem Units.map_comp

added theorem Units.map_id

added theorem Units.mul_liftRight_inv

added theorem Units.val_div_eq_div_val

added theorem Units.val_pow_eq_pow_val

added theorem Units.val_zpow_eq_zpow_val

added theorem divp_eq_div

added theorem eq_on_inv

added theorem isUnit_map_of_leftInverse

added theorem map_units_inv