Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-11-05 13:33 b31af6d9

View on Github →

refactor(algebra/group): move monoid.has_pow etc to algebra.group.defs (#10147) This way we can state theorems about pow/nsmul using notation ^ and • right away. Also move some ext lemmas to a new file and rewrite proofs using properties of monoid_homs.

Estimated changes

added theorem finset.prod_zpow
deleted theorem finset.zsmul_sum
modified theorem commute.is_unit_mul_iff
added theorem commute.pow_left
added theorem commute.pow_pow
added theorem commute.pow_pow_self
added theorem commute.pow_right
added theorem commute.pow_self
added theorem commute.self_pow
modified theorem commute.units_inv_left
modified theorem commute.units_inv_right
modified theorem commute.units_inv_right_iff
modified theorem is_unit_mul_self_iff
added theorem pow_succ'
deleted theorem cancel_comm_monoid.ext
deleted theorem cancel_monoid.ext
deleted theorem comm_group.ext
deleted theorem comm_monoid.ext
deleted theorem div_inv_monoid.ext
deleted theorem group.ext
deleted theorem left_cancel_monoid.ext
deleted theorem monoid.ext
deleted theorem npow_add
added theorem npow_eq_pow
deleted theorem npow_one
added theorem pow_succ
added theorem pow_zero
deleted theorem right_cancel_monoid.ext
added theorem zpow_coe_nat
added theorem zpow_eq_pow
added theorem zpow_neg_succ_of_nat
added theorem zpow_of_nat
added theorem zpow_zero
added theorem cancel_comm_monoid.ext
added theorem cancel_monoid.ext
added theorem comm_group.ext
added theorem comm_monoid.ext
added theorem div_inv_monoid.ext
added theorem group.ext
added theorem left_cancel_monoid.ext
added theorem monoid.ext
added theorem monoid_hom.map_div'
added theorem monoid_hom.map_pow
added theorem monoid_hom.map_zpow'
added theorem monoid_hom.map_zpow
added theorem semiconj_by.pow_right
deleted theorem commute.pow_left
deleted theorem commute.pow_pow
deleted theorem commute.pow_pow_self
deleted theorem commute.pow_right
deleted theorem commute.pow_self
deleted theorem commute.self_pow
deleted theorem monoid_hom.map_pow
deleted theorem npow_eq_pow
deleted theorem pow_succ'
deleted theorem pow_succ
deleted theorem pow_zero
deleted theorem semiconj_by.pow_right
deleted theorem zpow_coe_nat
deleted theorem zpow_eq_pow
deleted theorem zpow_neg_succ_of_nat
deleted theorem zpow_of_nat
deleted theorem zpow_zero
deleted theorem monoid_hom.map_zpow
modified def subgroup.saturated