Commit 2020-11-14 11:02 5f151043

View on Github →

feat(algebra/squarefree): Defines squarefreeness, proves several equivalences (#4981) Defines when a monoid element is squarefree Proves basic lemmas to determine squarefreeness Proves squarefreeness criteria in terms of multiplicity, unique_factorization_monoid.factors, and nat.factors

Estimated changes

Created src/algebra/squarefree.lean

added theorem irreducible.squarefree

added theorem is_unit.squarefree

added theorem multiplicity.squarefree_iff_multiplicity_le_one

added theorem nat.squarefree_iff_nodup_factors

added theorem not_squarefree_zero

added theorem prime.squarefree

added def squarefree

added theorem squarefree_of_dvd_of_squarefree

added theorem squarefree_one

added theorem unique_factorization_monoid.squarefree_iff_nodup_factors

Modified src/ring_theory/multiplicity.lean

added theorem multiplicity.multiplicity_le_multiplicity_of_dvd