Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-01-28 15:19
36dd6a66
View on Github →
feat(algebra/squarefree): squarefree iff no square irreducible divisors (
#11544
)
Estimated changes
Modified
src/algebra/squarefree.lean
added
theorem
irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree
added
theorem
nat.squarefree_iff_prime_sq_not_dvd
added
theorem
squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible
added
theorem
squarefree_iff_irreducible_sq_not_dvd_of_ne_zero