Theorems · Definition · commutative algebra
Squarefree
{R : Type u_1} → [Monoid R] → R → PropAn element of a monoid is squarefree if the only squares that divide it are the squares of units.
- Defined in
- Mathlib.Algebra.Squarefree.Basic
- Cited by
- 112 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 32 definitions · uses no axioms
- Assumes
- Monoid
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by120
Results whose statement or proof uses this declaration.
- ArithmeticFunction.moebiusproof · cited by 45
- Squarefree.ne_zerostatement and proof · cited by 18
- Squarefree.squarefree_of_dvdstatement and proof · cited by 15
- UniqueFactorizationMonoid.moebiusproof · cited by 10
- Nat.MinSqFacPropproof · cited by 7
- ArithmeticFunction.moebius_apply_of_squarefreestatement and proof · cited by 7
- Squarefree.isRadicalstatement and proof · cited by 7
- Nat.prod_primeFactors_of_squarefreestatement and proof · cited by 7
- Irreducible.squarefreestatement · cited by 6
- IsRadical.squarefreestatement · cited by 6
- BoundingSieve.prodPrimes_squarefreestatement · cited by 6
- Polynomial.Separable.squarefreestatement · cited by 6