Where to put Nat prime factorization theorem variant

Stream: mathlib4

[Johannes Choo]

In the course of contributing to Numina, I made the use of this version of the prime factorization theorem for Nats

import Mathlib
theorem prime_factorization (n : ℕ) (npos : n ≠ 0) : n = ∏ p ∈ n.primeFactors, p ^ (n.factorization p) := by
  calc
    n = id n := rfl
    _ = n.factorization.prod fun (p k : ℕ) => id (p ^ k) := by
      rw [Nat.multiplicative_factorization id]
      · intro x y _; simp
      · simp
      · exact npos
    _ = n.factorization.prod fun (p k : ℕ) => (p ^ k) := by simp
    _ = ∏ p ∈ n.primeFactors, p ^ (n.factorization p) := by
      rw [Nat.prod_factorization_eq_prod_primeFactors]

This is useful when reasoning about prime factorization without having to reason about list orderings as in primeFactorsList, which is presently the primary way the prime factorization theorem for nats is encoded in Mathlib.

I'd like for this to be in Mathlib (once golfed), but I'm not sure where it should reside. Note that Nat.multiplicative_factorization comes from Mathlib/Data/Nat/Factorization/Induction.lean while Nat.prod_factorization_eq_prod_primeFactors comes from Mathlib/Data/Nat/Factorization/Basic.lean; neither import the other. Present files that import both seem too specialized.

[Eric Wieser]

Here's the golfed version:

theorem prime_factorization (n : ℕ) (npos : n ≠ 0) : n = ∏ p ∈ n.primeFactors, p ^ (n.factorization p) :=
  Nat.factorization_prod_pow_eq_self npos |>.symm

[Johannes Choo]

Oh right, this is a quick specialization of that. In that case it could be added to Basic, but I wonder if this result would be useful.

[Eric Wieser]

I think the problem here is that there are too many ways to spell things, and I'm not sure adding more lemmas is the solution

[Eric Wieser]

Certainly it is not worth adding a lemma that just flips the direction of docs#Nat.factorization_prod_pow_eq_self, but indeed your statement does a little more than that, putting it in a grayer area

[Jireh Loreaux]

Why not have a rewrite lemma (proved with rfl) that rewrites between n.factorization.prod ... and Π p ∈ n.primeFactors, p ^ ...? That seems reasonable.

[Eric Wieser]

I think that lemma already exists, docs#Nat.prod_factorization_eq_prod_primeFactors

[Eric Wieser]

That is, the more instructive proof is:

theorem prime_factorization (n : ℕ) (npos : n ≠ 0) : n = ∏ p ∈ n.primeFactors, p ^ (n.factorization p) := by
  rw [← Nat.prod_factorization_eq_prod_primeFactors, Nat.factorization_prod_pow_eq_self npos]

[Jireh Loreaux]

So then arguably we don't need this lemma at all?