Help locating lemma: n.factorization.support = n.primeFactor

Stream: new members

[Bob Jefferson]

Hi all — I’m fairly new to working directly with the factorization API, and I’m trying to prove a simple lemma that I suspect already exists somewhere in mathlib.

My current goal is to show that if a prime doesn’t divide n, then it doesn’t appear in the support of the factorisation. Concretely:

lemma factorization_eq_zero_of_not_mem_primeFactors {n p : ℕ} (hp : p ∉ n.primeFactors) : n.factorization p = 0 := by ...

I thought there might be a lemma characterising the support, something like:

n.factorization.support = n.primeFactors

or at least a mem_support_iff specialised to the number-theory setting, but I can’t find anything obvious.

For reference, I’m working with mathlib pinned at:

30ceb3260d7d7536

If anyone can point me to the right lemma or the recommended approach, I’d be very grateful.
Thanks

[Mirek Olšák]

There are a few ways to search for lemmas.

1. exact? tactic

lemma factorization_eq_zero_of_not_mem_primeFactors {n p : ℕ} (hp : p ∉ n.primeFactors) :
  n.factorization p = 0 := by exact?

will search for a few seconds, and replies in the infoView with Try this: exact Finsupp.not_mem_support_iff.mp hp, you can click on it, and it will replace the exact? word.

[Mirek Olšák]

2. Loogle, you can search for theorems

• Containing specific set of constants: https://loogle.lean-lang.org/?q=Nat.primeFactors%2C+Nat.factorization
• Containing a specific subterm: https://loogle.lean-lang.org/?q=Nat.factorization+%3F_+%3F_+%3D+0

[Bob Jefferson]

Many thanks — this is very useful. I’ll try exact? together with Loogle to see what my pinned mathlib version actually provides. I’m specifically checking whether something like Nat.primeFactors_eq_toFinset exists in my snapshot; it appears to be present in newer mathlib but may not be available in the version I’m pinned to. If it isn’t, I’ll consider cloning the project and updating my pin. If that doesn't work I'll just construct a local lemma along the same lines. Appreciate the help!

[Mirek Olšák]

Indeed, loogle as a web service works with the up to date mathlib, and it is generally recommended to keep Lean up to date (but I am also guilty of keeping quite an old version on my computer). By the way, another local ways of searching for tactics are other questionmark tactics.

3. simp? doesn't work in your case but can be useful to see what simp used when it did something
4. rw??, if you write this tactic, shift-click on n.factorization p in the infoview, and wait for a few seconds, you get several suggestions such as

• Multiset.count p (Finsupp.toMultiset n.factorization)]()
• [if p ∈ n.factorization.support then n.factorization p else 0]()

[Bob Jefferson]

Thanks again, that’s really helpful.

I’m on a slightly older mathlib pin, so I don’t have some of the newer
primeFactors_eq_… lemmas, but your suggestions with exact?, simp? and
especially rw?? are exactly what I needed. Being able to point rw?? at
n.factorization p and see the “if p ∈ support then … else 0” shape (and the
multiset view) gives me a clear route to prove the lemma I want in my
current environment, even without upgrading mathlib right away.

[Snir Broshi]

Is this what you're asking for in the title?

import Mathlib
theorem foo (n : ℕ) : n.factorization.support = n.primeFactors := by
  rfl

This is true by definition, since docs#Nat.factorization looks like this:

def factorization (n : ℕ) : ℕ →₀ ℕ where
  support := n.primeFactors
  toFun p := if p.Prime then padicValNat p n else 0
  mem_support_toFun := by simp [not_or]; aesop

[Snir Broshi]

Also your lemma is very close to being true by definition of a finitely supported function:

import Mathlib
lemma factorization_eq_zero_of_not_mem_primeFactors {n p : ℕ} (hp : p ∉ n.primeFactors) :
    n.factorization p = 0 := by
  exact Finsupp.notMem_support_iff.mp hp

and it'll probably work on any Mathlib version (though the name of the theorem might differ)

[Snir Broshi]

Bob Jefferson said:

For reference, I’m working with mathlib pinned at:

30ceb3260d7d7536

There is no such Mathlib commit: https://github.com/leanprover-community/mathlib4/commit/30ceb3260d7d7536

[Bob Jefferson]

Hi, just a quick note to say thank you. Your observation that
n.factorization.support = n.primeFactors definitionally was exactly the breakthrough I needed.

I had been preparing to build a whole bridge via divisors, mem_divisors, etc., but your reminder that the support of Nat.factorization is already set to primeFactors meant the lemma

lemma factorization_eq_zero_of_not_mem_primeFactors …

was essentially immediate from Finsupp.notMem_support_iff.

That single insight massively simplified the design of my multiplicative-functions mini-library, and the τ multiplicativity file now builds cleanly. Really appreciated — thank you for taking the time to reply and point me in the right direction.