toFinsetFactors

Stream: mathlib4

[Arend Mellendijk]

The current idiom for "the finset of prime factors of n:Nat" is n.factors.toFinset. (n.factors is a list). @Johan Commelin pointed out that this set should probably have a name. I tend to agree. What should it be called?

[Arend Mellendijk]

/poll What should we call this set?

[Arend Mellendijk]

For reference:
@loogle Nat.factors, List.toFinset

[loogle]

:exclamation: <input>:1:13: expected end of input

[Arend Mellendijk]

@loogle Nat.factors, List.toFinset

[loogle]

:search: Nat.prime_divisors_eq_to_filter_divisors_prime, Nat.factors_mul_toFinset, and 13 more

[Antoine Chambert-Loir]

FactorsFinset

[Eric Wieser]

I'd be tempted to make this an abbrev so that it doesn't cost anything

[Adam Topaz]

I added n.support as an option, but maybe that's not too intuitive for most people.

[Adam Topaz]

note that support should also makes sense for (nonzero) rational numbers.

[Eric Rodriguez]

docs#Nat.factorization.support

[Eric Rodriguez]

whatever it is I think should be an abbrev of factorization.support

[Eric Wieser]

(docs#Nat.factorization, docs#Finsupp.support)

[Arend Mellendijk]

I just noticed docs#Nat.support_factorization is a simp lemma, suggesting n.factors.toFinset is currently the canonical spelling.

[Arend Mellendijk]

Either way, the fact that there are two very natural ways of expressing this concept makes me think this should be a def rather than an abbreviation.

[Eric Rodriguez]

But I think it's nice to apply stuff about finsupps - there was some good work put into the factorization stuff

[Arend Mellendijk]

If we're going with an abbreviation I'd like to consider what we want simp to do with p ∈ n.primeDivisors. Currently:

import Mathlib.Data.Nat.Factorization.Basic

abbrev primeDivisors (n : ℕ) : Finset ℕ := n.factorization.support

example (n p : ℕ) (h : p ∈ n.primeDivisors) : True := by
  simp at h
  /- h : p ∈ factors n -/
  trivial

/- And if we remove simp from support_factorization: -/
attribute [-simp] Nat.support_factorization
example (n p : ℕ) (h : p ∈ n.primeDivisors) : True := by
  simp at h
  /- h : ¬↑(factorization n) p = 0 -/
  trivial

I'd argue it would be much more natural to have a simp lemma like docs#Nat.mem_divisors that produces p.Prime ∧ p ∣ n ∧ n ≠ 0, but we can't do that with an abbreviation since simp could apply more general results like docs#List.mem_toFinset or docs#Finsupp.mem_support_iff first.

[Arend Mellendijk]

I've opened a #7607, which makes n.primeDivisorsan abbreviation for n.factorization.support and attempts to make it into the canonical spelling throughout mathlib. (that includes removing simp from support_factorization)