Commit 2023-05-18 13:08 c39117e4

View on Github →

feat: port NumberTheory.Multiplicity (#4044)

Estimated changes

Modified Mathlib.lean

Created Mathlib/NumberTheory/Multiplicity.lean

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 Nat.two_pow_sub_pow

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 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.geom_sum₂_eq_one

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 not_dvd_geom_sum₂

added theorem odd_sq_dvd_geom_sum₂_sub

added theorem padicValNat.pow_add_pow

added theorem padicValNat.pow_sub_pow

added theorem padicValNat.pow_two_sub_pow

added theorem pow_two_pow_sub_pow_two_pow

added theorem sq_dvd_add_pow_sub_sub