Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-08 13:42 700181a3

View on Github →

refactor(algebra/is_prime_pow): move lemmas using factorization to new file (#14598) As discussed in this Zulip thread.

Estimated changes

Modified src/algebra/is_prime_pow.lean

deleted theorem is_prime_pow.min_fac_pow_factorization_eq

deleted theorem is_prime_pow_iff_card_support_factorization_eq_one

deleted theorem is_prime_pow_iff_factorization_eq_single

deleted theorem is_prime_pow_iff_min_fac_pow_factorization_eq

deleted theorem is_prime_pow_iff_unique_prime_dvd

deleted theorem is_prime_pow_of_min_fac_pow_factorization_eq

deleted theorem is_prime_pow_pow_iff

deleted theorem nat.coprime.is_prime_pow_dvd_mul

deleted theorem nat.mul_divisors_filter_prime_pow

Renamed src/data/nat/factorization.lean to src/data/nat/factorization/basic.lean

Created src/data/nat/factorization/prime_pow.lean

added theorem is_prime_pow.min_fac_pow_factorization_eq

added theorem is_prime_pow_iff_card_support_factorization_eq_one

added theorem is_prime_pow_iff_factorization_eq_single

added theorem is_prime_pow_iff_min_fac_pow_factorization_eq

added theorem is_prime_pow_iff_unique_prime_dvd

added theorem is_prime_pow_of_min_fac_pow_factorization_eq

added theorem is_prime_pow_pow_iff

added theorem nat.coprime.is_prime_pow_dvd_mul

added theorem nat.mul_divisors_filter_prime_pow

Modified src/data/nat/squarefree.lean

Modified src/field_theory/cardinality.lean

Modified src/group_theory/nilpotent.lean

Modified src/group_theory/sylow.lean

Modified src/number_theory/arithmetic_function.lean

Modified src/number_theory/padics/padic_val.lean

Modified src/ring_theory/multiplicity.lean