Commit 2024-07-17 17:39 11d3bd21

View on Github →

chore: Rename Nat.factors to Nat.primeFactorsList (#13832) Nat.factors was a very generic name that didn't emphasize that

  • It is a list
  • It is not all factors but only the prime ones

Estimated changes

deleted theorem Nat.factors_count_eq
deleted theorem Nat.Prime.factors_pow
deleted theorem Nat.dvd_of_mem_factors
deleted theorem Nat.eq_of_perm_factors
deleted def Nat.factors
deleted theorem Nat.factors_add_two
deleted theorem Nat.factors_chain'
deleted theorem Nat.factors_chain
deleted theorem Nat.factors_chain_2
deleted theorem Nat.factors_eq_nil
deleted theorem Nat.factors_one
deleted theorem Nat.factors_prime
deleted theorem Nat.factors_sorted
deleted theorem Nat.factors_sublist_right
deleted theorem Nat.factors_subset_of_dvd
deleted theorem Nat.factors_subset_right
deleted theorem Nat.factors_two
deleted theorem Nat.factors_unique
deleted theorem Nat.factors_zero
deleted theorem Nat.le_of_mem_factors
deleted theorem Nat.mem_factors'
deleted theorem Nat.mem_factors
deleted theorem Nat.mem_factors_iff_dvd
deleted theorem Nat.mem_factors_mul
deleted theorem Nat.mem_factors_mul_left
deleted theorem Nat.mem_factors_mul_right
deleted theorem Nat.perm_factors_mul
deleted theorem Nat.pos_of_mem_factors
deleted theorem Nat.prime_of_mem_factors
deleted theorem Nat.prod_factors
modified def Nat.primeFactors
modified theorem Nat.toFinset_factors
deleted theorem Squarefree.nodup_factors
modified def Nat.factoredNumbers
modified theorem Nat.mem_smoothNumbers
modified theorem Nat.prod_mem_smoothNumbers
modified def Nat.smoothNumbers
modified theorem Nat.factors_eq