Theorems · Definition · commutative algebra
Ideal.IsRadical
{R : Type u} → [inst : CommSemiring R] → Ideal R → PropAn ideal is radical if it contains its radical.
- Defined in
- Mathlib.RingTheory.Ideal.Operations
- Cited by
- 30 results in Mathlib
- Foundations
- Depth 77 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- CommSemiring
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommSemiringstatement and proof · cited by 10,911
- Idealstatement and proof · cited by 4,748
- Ideal.radicalproof · cited by 121
Cited by32
Results whose statement or proof uses this declaration.
- Ideal.IsPrime.isRadicalstatement · cited by 14
- Ideal.IsRadical.radicalstatement · cited by 8
- Ideal.radical_isRadicalstatement · cited by 7
- IsJacobsonRing.outstatement · cited by 6
- Ideal.IsRadical.radical_le_iffstatement and proof · cited by 5
- isJacobsonRing_iff_prime_eqproof · cited by 5
- IsSemisimpleModule.annihilator_isRadicalstatement and proof · cited by 4
- Ideal.isRadical_botstatement · cited by 4
- Ideal.isRadical_iff_quotient_reducedstatement and proof · cited by 4
- PrimeSpectrum.isIrreducible_zeroLocus_iff_of_radicalstatement and proof · cited by 3
- isRadical_iff_span_singletonstatement and proof · cited by 3
- PrimeSpectrum.isJacobsonRing_iff_jacobsonSpaceproof · cited by 2