Theorems · Definition · commutative algebra
IsRadical
{R : Type u_1} → [Dvd R] → [Pow R ℕ] → R → PropAn element y in a monoid is radical if for any element x, y divides x whenever it
divides a power of x.
- Defined in
- Mathlib.RingTheory.Nilpotent.Defs
- Cited by
- 16 results in Mathlib
- Foundations
- Depth 4 from the axioms · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites0
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Nothing in Mathlib beyond the foundations.
Cited by16
Results whose statement or proof uses this declaration.
- Squarefree.isRadicalstatement · cited by 7
- IsRadical.squarefreestatement and proof · cited by 6
- isRadical_iff_pow_one_ltstatement and proof · cited by 3
- isRadical_iff_span_singletonstatement · cited by 3
- UniqueFactorizationMonoid.isRadical_radicalstatement · cited by 3
- minpoly.isRadicalstatement · cited by 2
- UniqueFactorizationMonoid.normalizedFactors_nodupstatement and proof · cited by 2
- isRadical_iff_squarefree_of_ne_zerostatement · cited by 1
- isRadical_iff_squarefree_or_zerostatement and proof · cited by 1
- UniqueFactorizationMonoid.primeFactors_val_eq_normalizedFactorsstatement and proof · cited by 1
- IsRadical.dvd_radicalstatement and proof · cited by 1
- zero_isRadical_iffstatement and proof · cited by 1