Commit 2024-05-13 11:45 cec3ec0b

View on Github →

chore: Delete Algebra.GroupWithZero.Power (#12825) After #12736, all lemmas in Algebra.GroupWithZero.Power can move to the earlier files where they belong. The changes to their proofs are minimal. It's just a matter of using the new Lean 4 Nat- and Int-specific lemmas instead of the generic algebraic order ones.

Estimated changes

added theorem div_sq_cancel
added theorem zero_zpow
added theorem zero_zpow_eq
added theorem zpow_add'
added theorem zpow_add_one₀
added theorem zpow_add₀
added theorem zpow_one_add₀
added theorem zpow_sub_one₀
added theorem pow_inv_comm₀
deleted theorem Commute.self_zpow₀
deleted theorem Commute.zpow_left₀
deleted theorem Commute.zpow_right₀
deleted theorem Commute.zpow_self₀
deleted theorem Commute.zpow_zpow_self₀
deleted theorem Commute.zpow_zpow₀
deleted theorem SemiconjBy.zpow_right₀
deleted theorem div_sq_cancel
deleted theorem eq_zero_of_zpow_eq_zero
deleted theorem inv_pow_sub_of_lt
deleted theorem inv_pow_sub₀
deleted theorem pow_inv_comm₀
deleted theorem pow_sub_of_lt
deleted theorem pow_sub₀
deleted theorem zero_zpow
deleted theorem zero_zpow_eq
deleted theorem zpow_add'
deleted theorem zpow_add_one₀
deleted theorem zpow_add₀
deleted theorem zpow_eq_zero_iff
deleted theorem zpow_ne_zero
deleted theorem zpow_ne_zero_iff
deleted theorem zpow_neg_mul_zpow_self
deleted theorem zpow_one_add₀
deleted theorem zpow_sub_one₀
deleted theorem zpow_sub₀
added theorem Commute.self_zpow₀
added theorem Commute.zpow_left₀
added theorem Commute.zpow_right₀
added theorem Commute.zpow_self₀
added theorem Commute.zpow_zpow₀
added theorem inv_pow_sub_of_lt
added theorem inv_pow_sub₀
added theorem pow_sub_of_lt
added theorem pow_sub₀
added theorem zpow_eq_zero_iff
added theorem zpow_ne_zero
added theorem zpow_ne_zero_iff
added theorem zpow_neg_mul_zpow_self
added theorem zpow_sub₀