Commit 2022-11-23 04:05 cbc08341

View on Github →

feat: port Algebra.Group.Units (#549) mathlib hash: 7cca171008afb30576d2d4c51173700a780c23d0

Estimated changes

added theorem IsUnit.exists_left_inv
added theorem IsUnit.mul
added theorem IsUnit.mul_iff
added theorem IsUnit.mul_left_inj
added theorem IsUnit.mul_right_inj
added theorem IsUnit.mul_val_inv
added theorem IsUnit.unit_spec
added theorem IsUnit.val_inv_mul
added def IsUnit
added def Units.copy
added theorem Units.copy_eq
added theorem Units.eq_iff
added theorem Units.ext
added theorem Units.ext_iff
added theorem Units.inv_eq_val_inv
added theorem Units.inv_mk
added theorem Units.inv_mul
added theorem Units.inv_mul_eq_one
added theorem Units.inv_mul_of_eq
added theorem Units.inv_unique
added theorem Units.isUnit_mul_units
added theorem Units.isUnit_units_mul
added theorem Units.mk_val
added theorem Units.mul_inv
added theorem Units.mul_inv_eq_one
added theorem Units.mul_inv_of_eq
added theorem Units.mul_left_inj
added theorem Units.mul_right_inj
added theorem Units.val_eq_one
added theorem Units.val_mk
added theorem Units.val_mkOfMulEqOne
added theorem Units.val_mul
added theorem Units.val_one
added def divp
added theorem divp_assoc'
added theorem divp_assoc
added theorem divp_divp_eq_divp_mul
added theorem divp_eq_divp_iff
added theorem divp_eq_iff_mul_eq
added theorem divp_eq_one_iff_eq
added theorem divp_inv
added theorem divp_left_inj
added theorem divp_mul_cancel
added theorem divp_mul_divp
added theorem divp_mul_eq_mul_divp
added theorem divp_one
added theorem divp_self
added theorem eq_divp_iff_mul_eq
added theorem inv_eq_one_divp'
added theorem inv_eq_one_divp
added theorem isUnit_iff_exists_inv'
added theorem isUnit_iff_exists_inv
added theorem isUnit_of_mul_eq_one
added theorem isUnit_of_subsingleton
added theorem isUnit_one
added theorem mul_divp_cancel
added theorem one_divp
added theorem unique_one
added theorem val_div_eq_divp