def Nat.squarefreePart (n : ℕ) : ℕ

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.

Equations

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

theorem Nat.squarefreePart_ne_zero (n : ℕ) : n.squarefreePart ≠ 0

theorem Nat.squarefreePart_zero : squarefreePart 0 = 1

theorem Nat.squarefreePart_of_squarefree {n : ℕ} (hn : Squarefree n) : n.squarefreePart = n

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

theorem Nat.squarefreePart_of_isSquare {n : ℕ} (hn : IsSquare n) : n.squarefreePart = 1

The squarefree part of any square is 1.

theorem Nat.squarefreePart_factorization (n : ℕ) {p : ℕ} (hp : Prime p) : n.squarefreePart.factorization p = n.factorization p % 2

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 Nat.Prime.squarefree {p : ℕ} (hp : Prime p) : Squarefree p

theorem Nat.squarefree_squarefreePart (n : ℕ) : Squarefree n.squarefreePart

theorem Nat.squarefreePart_dvd (n : ℕ) : n.squarefreePart ∣ n

def Nat.squarePart (n : ℕ) : ℕ

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

Equations

• n.squarePart = n / n.squarefreePart

theorem Nat.squarePart_zero : squarePart 0 = 0

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

The squarefree decomposition of a natural number.