Commit 2023-03-21 21:27 98e7a89e

View on Github →

feat: port Algebra.Squarefree (#3018)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Squarefree.lean

added theorem Irreducible.squarefree

added theorem IsRadical.squarefree

added theorem IsUnit.squarefree

added theorem Prime.squarefree

added theorem Squarefree.gcd_left

added theorem Squarefree.gcd_right

added theorem Squarefree.isRadical

added theorem Squarefree.ne_zero

added theorem Squarefree.of_mul_left

added theorem Squarefree.of_mul_right

added theorem Squarefree.squarefree_of_dvd

added def Squarefree

added theorem UniqueFactorizationMonoid.dvd_pow_iff_dvd_of_squarefree

added theorem UniqueFactorizationMonoid.squarefree_iff_nodup_normalizedFactors

added theorem irreducible_sq_not_dvd_iff_eq_zero_and_no_irreducibles_or_squarefree

added theorem isRadical_iff_squarefree_of_ne_zero

added theorem isRadical_iff_squarefree_or_zero

added theorem multiplicity.finite_prime_left

added theorem multiplicity.squarefree_iff_multiplicity_le_one

added theorem not_squarefree_zero

added theorem squarefree_iff_irreducible_sq_not_dvd_of_exists_irreducible

added theorem squarefree_iff_irreducible_sq_not_dvd_of_ne_zero

added theorem squarefree_one