Commit 2023-01-02 19:20 79880b28

View on Github →

feat: port algebra.group_with_zero.power (#1251)

Estimated changes

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 div_sq_cancel
added theorem inv_pow_sub_of_lt
added theorem inv_pow_sub₀
added theorem map_zpow₀
added theorem pow_inv_comm₀
added theorem pow_sub_of_lt
added theorem pow_sub₀
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_bit1'
added theorem zpow_bit1₀
added theorem zpow_eq_zero
added theorem zpow_eq_zero_iff
added theorem zpow_ne_zero
added theorem zpow_neg_mul_zpow_self
added theorem zpow_one_add₀
added theorem zpow_sub_one₀
added theorem zpow_sub₀