Theorems · Theorem · commutative algebra
IsRadical.squarefree
∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x : R}, x ≠ 0 → IsRadical x → Squarefree x- Defined in
- Mathlib.Algebra.Squarefree.Basic
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- one_mulproof · cited by 2,841
- mul_assocproof · cited by 1,667
- CommMonoidWithZerostatement and proof · cited by 913
- mul_left_commproof · cited by 184
- IsCancelMulZerostatement and proof · cited by 177
- pow_twoproof · cited by 150
- Squarefreestatement · cited by 112
- mul_ne_zero_iffproof · cited by 39
- isUnit_iff_dvd_oneproof · cited by 21
- IsRadicalstatement and proof · cited by 16
- mul_dvd_mul_iff_rightproof · cited by 8
Cited by6
Results whose statement or proof uses this declaration.
- Module.End.IsSemisimple.of_mem_adjoin_pairproof · cited by 3
- Module.End.IsSemisimple.minpoly_squarefreeproof · cited by 2
- isRadical_iff_squarefree_of_ne_zeroproof · cited by 1
- isRadical_iff_squarefree_or_zeroproof · cited by 1
- Module.End.IsSemisimple.aevalproof · cited by 1
- UniqueFactorizationMonoid.squarefree_radicalproof · cited by 0