FormalConjecturesForMathlib.Data.Nat.Squarefree

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Data.Nat.Squarefree
public import FormalConjecturesForMathlib.Data.Nat.Factorization.Basic

public meta import Mathlib.Data.Nat.Factorization.Basic

import Mathlib.Tactic

@[expose] public sectionnamespace Nat

n.squarefreePart is the unique a₀ : ℕ such that a₀ is squarefree and n = a₀ * b ^ 2, for some b : ℕ. At 0 this property is not well defined because b must be 0 and a₀ can be any squarefree number; we give the junk value 1 at n = 0 following the convention that the squarefree part of any square is 1.

def squarefreePart (n : ℕ) : ℕ := n.factorization.prod fun (p e : ℕ) ↦ p ^ (e % 2)

example : squarefreePart 2 = 2 := by⊢ squarefreePart 2 = 2
  decide +nativeAll goals completed! 🐙

example : squarefreePart 5 = 5 := by⊢ squarefreePart 5 = 5
  decide +nativeAll goals completed! 🐙

example : squarefreePart 4 = 1 := by⊢ squarefreePart 4 = 1
  decide +nativeAll goals completed! 🐙

example : squarefreePart 8 = 2 := by⊢ squarefreePart 8 = 2
  decide +nativeAll goals completed! 🐙

example : squarefreePart 16 = 1 := by⊢ squarefreePart 16 = 1
  decide +nativeAll goals completed! 🐙

example : squarefreePart 24 = 6 := by⊢ squarefreePart 24 = 6
  decide +nativeAll goals completed! 🐙

theorem squarefreePart_ne_zero (n : ℕ) : n.squarefreePart ≠ 0 := byn:ℕ⊢ n.squarefreePart ≠ 0
  simp [squarefreePart]All goals completed! 🐙

theorem squarefreePart_zero : squarefreePart 0 = 1 := by⊢ squarefreePart 0 = 1
  simp [squarefreePart]All goals completed! 🐙

If n is squarefree, then its squarefree part is itself.


theorem squarefreePart_of_squarefree {n : ℕ} (hn : Squarefree n) :
    squarefreePart n = n := byn:ℕhn:Squarefree n⊢ n.squarefreePart = n
  nth_rw 2 [← n.prod_factorization_pow_eq_self fun _ ↦ byn:ℕhn:Squarefree nx✝:n = 0⊢ False simp_allAll goals completed! 🐙]n:ℕhn:Squarefree n⊢ n.squarefreePart = n.factorization.prod fun x1 x2 ↦ x1 ^ x2
  simp only [squarefreePart, Finsupp.prod, support_factorization]n:ℕhn:Squarefree n⊢ ∏ a ∈ n.primeFactors, a ^ (n.factorization a % 2) = ∏ a ∈ n.primeFactors, a ^ n.factorization a
  exact Finset.prod_congr rfl fun p hp ↦ byn:ℕhn:Squarefree np:ℕhp:p ∈ n.primeFactors⊢ p ^ (n.factorization p % 2) = p ^ n.factorization p
    rw [factorization_eq_one_of_squarefree hn (mem_primeFactors.1 hp).1 (mem_primeFactors.1 hp).2.1n:ℕhn:Squarefree np:ℕhp:p ∈ n.primeFactors⊢ p ^ (1 % 2) = p ^ 1All goals completed! 🐙]All goals completed! 🐙

The squarefree part of any square is 1.


theorem squarefreePart_of_isSquare {n : ℕ} (hn : IsSquare n) :
    squarefreePart n = 1 := byn:ℕhn:IsSquare n⊢ n.squarefreePart = 1
  rcases eq_or_ne n 0 with (rfl | h₀)inlhn:IsSquare 0⊢ squarefreePart 0 = 1inrn:ℕhn:IsSquare nh₀:n ≠ 0⊢ n.squarefreePart = 1; exact squarefreePart_zeroinrn:ℕhn:IsSquare nh₀:n ≠ 0⊢ n.squarefreePart = 1
  obtain ⟨r, rfl⟩ := hninrr:ℕh₀:r * r ≠ 0⊢ (r * r).squarefreePart = 1
  rw [ne_eq,inrr:ℕh₀:¬r * r = 0⊢ (r * r).squarefreePart = 1inrr:ℕh₀:¬r = 0⊢ (r * r).squarefreePart = 1 mul_eq_zero,inrr:ℕh₀:¬(r = 0 ∨ r = 0)⊢ (r * r).squarefreePart = 1inrr:ℕh₀:¬r = 0⊢ (r * r).squarefreePart = 1 or_selfinrr:ℕh₀:¬r = 0⊢ (r * r).squarefreePart = 1inrr:ℕh₀:¬r = 0⊢ (r * r).squarefreePart = 1] at h₀inrr:ℕh₀:¬r = 0⊢ (r * r).squarefreePart = 1
  rw [squarefreePart,inrr:ℕh₀:¬r = 0⊢ ((r * r).factorization.prod fun p e ↦ p ^ (e % 2)) = 1inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1 Finsupp.prod,inrr:ℕh₀:¬r = 0⊢ ∏ a ∈ (r * r).factorization.support, a ^ ((r * r).factorization a % 2) = 1inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1 support_factorization,inrr:ℕh₀:¬r = 0⊢ ∏ a ∈ (r * r).primeFactors, a ^ ((r * r).factorization a % 2) = 1inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1
    Finset.prod_congr rfl fun p hp ↦ byr:ℕh₀:¬r = 0p:ℕhp:p ∈ (r * r).primeFactors⊢ p ^ ((r * r).factorization p % 2) = ?m.84 pinrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1 rw [r.factorization_mul h₀ h₀r:ℕh₀:¬r = 0p:ℕhp:p ∈ (r * r).primeFactors⊢ p ^ ((r.factorization + r.factorization) p % 2) = ?m.84 pAll goals completed! 🐙inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1]All goals completed! 🐙inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1]inrr:ℕh₀:¬r = 0⊢ ∏ p ∈ (r * r).primeFactors, p ^ ((r.factorization + r.factorization) p % 2) = 1
  simp [← two_mul]All goals completed! 🐙

If $n = \prod_p p^{e_p}$ is the prime factorization of $n$, then $\prod_p p^{e_p \pmod{2}}$ is the prime factorization of the squarefree part of $n$.


theorem squarefreePart_factorization (n : ℕ) {p : ℕ} (hp : p.Prime) :
    n.squarefreePart.factorization p = n.factorization p % 2 := byn:ℕp:ℕhp:Prime p⊢ n.squarefreePart.factorization p = n.factorization p % 2
  rw [squarefreePart,n:ℕp:ℕhp:Prime p⊢ (n.factorization.prod fun p e ↦ p ^ (e % 2)).factorization p = n.factorization p % 2All goals completed! 🐙 prod_factorization_eq_prod_primeFactors,n:ℕp:ℕhp:Prime p⊢ (∏ p ∈ n.primeFactors, p ^ (n.factorization p % 2)).factorization p = n.factorization p % 2All goals completed! 🐙
    n.prod_primeFactors_factorization_apply hp (f := fun p n ↦ n.factorization p % 2)
      (fun _ _ h ↦ byn:ℕp:ℕhp:Prime px✝¹:ℕx✝:ℕh:¬x✝¹ ∣ x✝⊢ x✝.factorization x✝¹ % 2 = 0All goals completed! 🐙 simp [factorization_eq_zero_of_not_dvd h]All goals completed! 🐙All goals completed! 🐙) (byn:ℕp:ℕhp:Prime p⊢ ∀ (q : ℕ), (factorization 0) q % 2 = 0All goals completed! 🐙 simpAll goals completed! 🐙All goals completed! 🐙)]All goals completed! 🐙

theorem Prime.squarefree {p : ℕ} (hp : p.Prime) : Squarefree p := Irreducible.squarefree hp

theorem squarefree_squarefreePart (n : ℕ) : Squarefree n.squarefreePart := byn:ℕ⊢ Squarefree n.squarefreePart
  refine Nat.squarefree_iff_factorization_le_one n.squarefreePart_ne_zero |>.2 fun p ↦ ?_n:ℕp:ℕ⊢ n.squarefreePart.factorization p ≤ 1
  by_cases hp : p.Primeposn:ℕp:ℕhp:Prime p⊢ n.squarefreePart.factorization p ≤ 1negn:ℕp:ℕhp:¬Prime p⊢ n.squarefreePart.factorization p ≤ 1
  ·posn:ℕp:ℕhp:Prime p⊢ n.squarefreePart.factorization p ≤ 1 linarith [n.squarefreePart_factorization hp, Nat.mod_lt (n.factorization p) two_pos]All goals completed! 🐙
  ·negn:ℕp:ℕhp:¬Prime p⊢ n.squarefreePart.factorization p ≤ 1 linarith [factorization_eq_zero_of_not_prime n.squarefreePart hp]All goals completed! 🐙

theorem squarefreePart_dvd (n : ℕ) : squarefreePart n ∣ n := byn:ℕ⊢ n.squarefreePart ∣ n
  rcases eq_or_ne n 0 with (rfl | h₀)inl⊢ squarefreePart 0 ∣ 0inrn:ℕh₀:n ≠ 0⊢ n.squarefreePart ∣ n; simpinrn:ℕh₀:n ≠ 0⊢ n.squarefreePart ∣ n
  exact Nat.factorization_prime_le_iff_dvd n.squarefreePart_ne_zero h₀ |>.1 fun p hp ↦
    squarefreePart_factorization _ hp ▸ Nat.mod_le _ _All goals completed! 🐙

The square part is the value of b ^ 2 in the squarefree decomposition of n = a₀ * b ^ 2.

def squarePart (n : ℕ) : ℕ := n / n.squarefreeParttheorem squarePart_zero : squarePart 0 = 0 := by⊢ squarePart 0 = 0 simp [squarePart]All goals completed! 🐙

The squarefree decomposition of a natural number.

theorem squarefreePart_mul_squarePart (n : ℕ) : n.squarefreePart * n.squarePart = n :=
  Nat.mul_div_eq_iff_dvd.2 n.squarefreePart_dvd

theorem squarefree_infinite : Set.Infinite { n : ℕ | Squarefree n } :=
  Set.Infinite.mono (fun _ hp ↦ hp.squarefree) Nat.infinite_setOfPred_prime

end Nat