Commit 2023-01-22 09:12 76059c49

View on Github →

feat: port Data.Nat.PrimeFin (#1759)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Nat/PrimeFin.lean

added theorem Nat.factors_mul_toFinset

added theorem Nat.factors_mul_toFinset_of_coprime

added theorem Nat.infinite_setOf_prime

added theorem Nat.pow_factors_toFinset

added theorem Nat.pow_succ_factors_toFinset

added theorem Nat.prime_pow_prime_divisor