Help needed on a proof that seems to involve factorization

Stream: new members

[Kevin Cheung]

I wonder how I should proceed in the following:

import Mathlib.Data.Nat.Factorization.Basic

example : (∀ k, 2 ∣ ((Nat.factorization n) k)) ↔ ∃ a, n = a ^ 2 := by
  constructor
  . sorry
  . intro ⟨ a, ha ⟩
    intro k
    rw [ha]
    rw [Nat.factorization_pow]
    dsimp
    apply exists_apply_eq_apply'

Insights or pointers greatly appreciated.

[Ruben Van de Velde]

You're missing some imports

[Kevin Cheung]

I had the following: import Mathlib.Data.Nat.Factorization.Basic

[Ruben Van de Velde]

Please edit your first message to include it

[Kevin Cheung]

Added the import.

[Ruben Van de Velde]

import Mathlib.Data.Nat.Factorization.Basic

example : (∀ k, 2 ∣ ((Nat.factorization n) k)) ↔ ∃ a, n = a ^ 2 := by
  constructor
  . intro h
    by_cases n = 0
    · use 0
      subst n
      simp
    use (Nat.factorization n).prod fun a b => a ^ ((Nat.factorization n) a / 2)
    rw [@Nat.prod_factorization_eq_prod_primeFactors]
    trans Finset.prod n.primeFactors fun x => x ^ ((Nat.factorization n) x)
    · rw [← @Nat.prod_factorization_eq_prod_primeFactors]
      rwa [Nat.factorization_prod_pow_eq_self]
    · rw [← @Finset.prod_pow]
      apply Finset.prod_congr rfl fun k _ => ?_
      rw [← pow_mul, Nat.div_mul_cancel (h k)]
  . intro ⟨ a, ha ⟩
    intro k
    rw [ha]
    rw [Nat.factorization_pow]
    dsimp
    apply exists_apply_eq_apply'

[Kevin Cheung]

Thank you. This looks a lot harder than I expected.

[Kevin Cheung]

Where can one find more examples of proofs using Nat.factorization and related theorems?

[Ruben Van de Velde]

I use loogle: https://loogle.lean-lang.org/?q=Nat.factorization

[Ruben Van de Velde]

It does feel like there's some lemmas missing

[Kevin Cheung]

You mean the library should have more results that people like me can use?

[Ruben Van de Velde]

Yeah, exactly.

[Eric Wieser]

Maybe the mathlib result should be in terms of Even (Nat.factorization n)?

[Eric Wieser]

With IsSquare on the RHS

[Eric Wieser]

Probably there's some low hanging fruit here for lemmas about Even / IsSquare on Pi/Prod/Finsupp etc

[Kevin Cheung]

Maybe a result like this could be added?

theorem some_name (d : Nat) (h : d > 0) : (∀ k, d ∣ ((Nat.factorization n) k)) ↔ ∃ a, n = a ^ d := sorry

[Yaël Dillies]

I think we basically have this in the form of docs#Nat.floorRoot

[Yaël Dillies]

Not entirely sure how painful the glue is