Theorems · Inductive type · commutative algebra
Ideal.IsMaximal
{α : Type u} → [inst : Semiring α] → Ideal α → PropAn ideal is maximal if it is maximal in the collection of proper ideals.
- Defined in
- Mathlib.RingTheory.Ideal.Maximal
- Cited by
- 452 results in Mathlib
- Foundations
- Depth 15 from the axioms, rests on 127 definitions · uses no axioms
- Assumes
- Semiring
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 by480
Results whose statement or proof uses this declaration.
- Ideal.jacobsonproof · cited by 88
- Ideal.IsMaximal.isPrimestatement and proof · cited by 53
- Ideal.exists_le_maximalstatement and proof · cited by 47
- Ideal.IsMaximal.ne_topstatement and proof · cited by 42
- Ideal.IsMaximal.eq_of_lestatement and proof · cited by 39
- Ideal.Quotient.fieldstatement and proof · cited by 25
- Ideal.IsPrime.isMaximalstatement · cited by 24
- IsLocalRing.le_maximalIdealproof · cited by 20
- IsLocalRing.eq_maximalIdealstatement and proof · cited by 20
- Ideal.IsMaximal.outstatement and proof · cited by 16
- IsLocalRing.maximalIdeal_le_jacobsonproof · cited by 16
- Ideal.isMaximal_defstatement and proof · cited by 11
Showing the 200 most cited of 480.