Commit 2024-07-12 10:19 fffcdb50

View on Github →

fix: rewrite Int.eq_pow_of_mul_eq_pow_* lemmas in terms of Odd (#14671)

Estimated changes

Modified Mathlib/RingTheory/Int/Basic.lean

deleted theorem Int.eq_pow_of_mul_eq_pow_bit1

deleted theorem Int.eq_pow_of_mul_eq_pow_bit1_left

deleted theorem Int.eq_pow_of_mul_eq_pow_bit1_right

added theorem Int.eq_pow_of_mul_eq_pow_odd

added theorem Int.eq_pow_of_mul_eq_pow_odd_left

added theorem Int.eq_pow_of_mul_eq_pow_odd_right