[Merged by Bors] - chore: Rename Nat.factors to Nat.primeFactorsList

[YaelDillies]

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

---

[github-actions]

PR summary b27a025c06

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.NumberTheory.Divisors	583	585	+2 (+0.34%)
Mathlib.NumberTheory.Padics.PadicVal	710	712	+2 (+0.28%)

Import changes for all files

Files	Import difference
9 files Mathlib.NumberTheory.Padics.PadicIntegers Mathlib.NumberTheory.Multiplicity Mathlib.SetTheory.Cardinal.Divisibility Mathlib.NumberTheory.Padics.PadicNumbers Mathlib.RingTheory.ChainOfDivisors Mathlib.NumberTheory.Harmonic.Int Mathlib.Data.Finset.NatDivisors Mathlib.NumberTheory.Padics.RingHoms Mathlib.NumberTheory.Padics.Hensel	1
4 files Mathlib.NumberTheory.Padics.PadicNorm Mathlib.Algebra.IsPrimePow Mathlib.NumberTheory.Divisors Mathlib.NumberTheory.Padics.PadicVal	2

---

Declarations diff

+ Prime.primeFactorsList_pow
+ Squarefree.nodup_primeFactorsList
+ coprime_primeFactorsList_disjoint
+ dvd_of_mem_primeFactorsList
+ dvd_of_primeFactorsList_subperm
+ eq_of_perm_primeFactorsList
+ factorization_eq_primeFactorsList_multiset
+ le_multiplicity_iff_replicate_subperm_primeFactorsList
+ le_of_mem_primeFactorsList
+ le_padicValNat_iff_replicate_subperm_primeFactorsList
+ mem_primeFactorsList
+ mem_primeFactorsList'
+ mem_primeFactorsList_iff_dvd
+ mem_primeFactorsList_mul
+ mem_primeFactorsList_mul_left
+ mem_primeFactorsList_mul_of_coprime
+ mem_primeFactorsList_mul_right
+ mem_primeFactors_iff_mem_primeFactorsList
+ perm_primeFactorsList_mul
+ perm_primeFactorsList_mul_of_coprime
+ pos_of_mem_primeFactorsList
+ primeFactorsList
+ primeFactorsList_add_two
+ primeFactorsList_chain
+ primeFactorsList_chain'
+ primeFactorsList_chain_2
+ primeFactorsList_count_eq
+ primeFactorsList_eq_nil
+ primeFactorsList_one
+ primeFactorsList_prime
+ primeFactorsList_sorted
+ primeFactorsList_sublist_of_dvd
+ primeFactorsList_sublist_right
+ primeFactorsList_subset_of_dvd
+ primeFactorsList_subset_right
+ primeFactorsList_two
+ primeFactorsList_unique
+ primeFactorsList_zero
+ primeFactors_eq_to_filter_divisors_prime
+ primeFactors_filter_dvd_of_dvd
+ prime_of_mem_primeFactorsList
+ prod_primeFactorsList
+ replicate_subperm_primeFactorsList_iff
+ squarefree_iff_nodup_primeFactorsList
- Prime.factors_pow
- coprime_factors_disjoint
- dvd_of_factors_subperm
- dvd_of_mem_factors
- eq_of_perm_factors
- factors_add_two
- factors_chain
- factors_chain'
- factors_chain_2
- factors_eq_nil
- factors_one
- factors_prime
- factors_sorted
- factors_sublist_of_dvd
- factors_sublist_right
- factors_subset_of_dvd
- factors_subset_right
- factors_two
- factors_unique
- factors_zero
- le_of_mem_factors
- mem_factors
- mem_factors'
- mem_factors_iff_dvd
- mem_factors_mul
- mem_factors_mul_left
- mem_factors_mul_of_coprime
- mem_factors_mul_right
- perm_factors_mul
- perm_factors_mul_of_coprime
- pos_of_mem_factors
- prime_of_mem_factors
- prod_factors
- replicate_subperm_factors_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[Ruben-VandeVelde]

Can you limit this PR to the renaming?

[YaelDillies]

What am I doing that is not the renaming?

[BoltonBailey]

Perhaps Ruben is confused that this changes not just factors but every lemma name that referenced factors as a substring? I don't think it makes sense to change those in a different PR though, this looks good to me.

[YaelDillies]

I should say that I am not particularly attached to the name primeFactorsList and I would be happy to hear alternatives.

[kim-em]

Assuming the merge conflict doesn't cause anything unexpected:

bors d+

[mathlib-bors]

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[YaelDillies]

Was a trivial fix

bors merge

[mathlib-bors]

👎 Rejected by label

[YaelDillies]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style