Squarefree rationals

This file gathers results about squarefreeness and rational numbers.

Main results

• Rat.sq_mul_squarefree_unique: the squarefree integer d in such a decomposition is unique.

theorem Rat.sq_mul_squarefree_unique {d₁ d₂ : ℤ} (h₁ : Squarefree d₁) (h₂ : Squarefree d₂) (r₁ r₂ : ℚ) (hr₁ : r₁ ≠ 0) (h : r₁ ^ 2 * ↑d₁ = r₂ ^ 2 * ↑d₂) : d₁ = d₂

The squarefree integer d in a decomposition q = r ^ 2 * d is unique.