Commit 2022-09-29 10:48 7944d185

View on Github →

feat(number_theory/multiplicity): lifting the exponent lemma (#8915) multiplicity.int.pow_sub_pow is the lifting the exponent lemma for odd primes. Some variations are also proved.

Estimated changes

Modified src/algebra/geom_sum.lean

added theorem geom_sum₂_comm

Created src/number_theory/multiplicity.lean

added theorem dvd_geom_sum₂_iff_of_dvd_sub'

added theorem dvd_geom_sum₂_iff_of_dvd_sub

added theorem dvd_geom_sum₂_self

added theorem int.sq_mod_four_eq_one_of_odd

added theorem int.two_pow_sub_pow'

added theorem int.two_pow_sub_pow

added theorem int.two_pow_two_pow_add_two_pow_two_pow

added theorem int.two_pow_two_pow_sub_pow_two_pow

added theorem multiplicity.geom_sum₂_eq_one

added theorem multiplicity.int.pow_add_pow

added theorem multiplicity.int.pow_sub_pow

added theorem multiplicity.nat.pow_add_pow

added theorem multiplicity.nat.pow_sub_pow

added theorem multiplicity.pow_prime_pow_sub_pow_prime_pow

added theorem multiplicity.pow_prime_sub_pow_prime

added theorem multiplicity.pow_sub_pow_of_prime

added theorem nat.two_pow_sub_pow

added theorem not_dvd_geom_sum₂

added theorem odd_sq_dvd_geom_sum₂_sub

added theorem padic_val_nat.pow_add_pow

added theorem padic_val_nat.pow_sub_pow

added theorem padic_val_nat.pow_two_sub_pow

added theorem pow_two_pow_sub_pow_two_pow

added theorem sq_dvd_add_pow_sub_sub