Commit 2023-11-10 09:14 5ced22e4

View on Github →

refactor: Unify spelling of "prime factors" (#8164) mathlib can't make up its mind on whether to spell "the prime factors of n" as n.factors.toFinset or n.factorization.support, even though those two are defeq. This PR proposes to unify everything to a new definition Nat.primeFactors, and streamline the existing scattered API about n.factors.toFinset and n.factorization.support to Nat.primeFactors. We also get to write a bit more API that didn't make sense before, eg primeFactors_mono.

Estimated changes

modified theorem Nat.support_factorization
added theorem Nat.mem_factors'
deleted theorem Nat.factors_mul_toFinset
added theorem Nat.mem_primeFactors
deleted theorem Nat.pow_factors_toFinset
added def Nat.primeFactors
added theorem Nat.primeFactors_gcd
added theorem Nat.primeFactors_mono
added theorem Nat.primeFactors_mul
added theorem Nat.primeFactors_one
added theorem Nat.primeFactors_pow
added theorem Nat.primeFactors_zero
added theorem Nat.toFinset_factors