Theorems · Definition · commutative algebra
IsLocalRing.maximalIdeal
(R : Type u_1) → [inst : CommSemiring R] → [IsLocalRing R] → Ideal R
The ideal of elements that are not units.
- Cited by
- 297 results in Mathlib
- Foundations
- Depth 26 from the axioms, rests on 288 definitions · uses propext
- Assumes
- CommSemiringIsLocalRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
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 · cited by 4,748
- AddSubmonoidproof · cited by 1,178
- IsLocalRingstatement and proof · cited by 339
- IsLocalRing.nonunitsAddSubmonoidproof · cited by 1
Cited by329
Results whose statement or proof uses this declaration.
- IsLocalRing.ResidueFieldproof · cited by 156
- IsLocalRing.residueproof · cited by 71
- IsLocalRing.closedPointproof · cited by 60
- IsDiscreteValuationRing.maximalIdealproof · cited by 25
- IsLocalRing.eq_maximalIdealstatement · cited by 20
- IsLocalRing.le_maximalIdealstatement · cited by 20
- Localization.AtPrime.map_eq_maximalIdealstatement and proof · cited by 17
- IsLocalRing.CotangentSpaceproof · cited by 16
- IsLocalRing.ResidueField.mapproof · cited by 16
- IsLocalRing.maximalIdeal_le_jacobsonstatement and proof · cited by 16
- PowerSeries.IsWeierstrassFactorizationproof · cited by 13
- PowerSeries.IsWeierstrassDivisor.of_map_ne_zeroproof · cited by 11
Showing the 200 most cited of 329.