The squarefree part of a natural number is unique #
A candidate for Mathlib.Data.Nat.Squarefree: d k ^ 2 = d' k' ^ 2 with d and d' squarefree
and k' ≠ 0 forces d = d', the uniqueness that complements Nat.sq_mul_squarefree_of_pos.
Main statements #
Nat.eq_of_mul_sq_eq_mul_sq: squarefree numbers times squares agree only for equal squarefree parts.
theorem
Nat.eq_of_mul_sq_eq_mul_sq
{d d' k k' : ℕ}
(hd : Squarefree d)
(hd' : Squarefree d')
(hk' : k' ≠ 0)
(h : d * k ^ 2 = d' * k' ^ 2)
:
The squarefree part is unique: d k ^ 2 = d' k' ^ 2 with d, d' squarefree and
k' ≠ 0 gives d = d', since d d' is then a square
(Squarefree.associated_of_isSquare_mul).