Commit 2023-03-29 02:11 e0405922

View on Github →

feat: port Data.Nat.Factorization.PrimePow (#3157)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/Factorization/PrimePow.lean

added theorem IsPrimePow.exists_ord_compl_eq_one

added theorem IsPrimePow.minFac_pow_factorization_eq

added theorem Nat.coprime.isPrimePow_dvd_mul

added theorem Nat.mul_divisors_filter_prime_pow

added theorem exists_ord_compl_eq_one_iff_isPrimePow

added theorem isPrimePow_iff_card_support_factorization_eq_one

added theorem isPrimePow_iff_factorization_eq_single

added theorem isPrimePow_iff_minFac_pow_factorization_eq

added theorem isPrimePow_iff_unique_prime_dvd

added theorem isPrimePow_of_minFac_pow_factorization_eq

added theorem isPrimePow_pow_iff