Theorems · Inductive type · commutative algebra
IsRegularLocalRing
(R : Type u_1) → [CommRing R] → Prop
A Noetherian local ring is said to be regular if its maximal ideal
can be generated by dim R elements.
- Defined in
- Mathlib.RingTheory.RegularLocalRing.Defs
- Cited by
- 8 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement · cited by 17,173
Cited by12
Results whose statement or proof uses this declaration.
- isRegularLocalRing_iffstatement and proof · cited by 4
- IsRegularLocalRing.of_ringEquivstatement and proof · cited by 2
- isRegularRing_iffstatement and proof · cited by 1
- IsRegularLocalRing.of_spanFinrank_maximalIdeal_lestatement · cited by 1
- Polynomial.isRegularLocalRing_localization_atPrime_of_comap_eq_maximalIdealstatement and proof · cited by 0
- IsRegularLocalRing.casesOnstatement and proof · cited by 0
- IsRegularLocalRing.iff_finrank_cotangentSpacestatement · cited by 0
- IsRegularLocalRing.of_isRegularRing_of_isLocalRingstatement · cited by 0
- IsRegularLocalRing.recOnstatement and proof · cited by 0
- IsRegularLocalRing.spanFinrank_maximalIdealstatement and proof · cited by 0
- IsRegularRing.casesOnstatement and proof · cited by 0
- IsRegularRing.recOnstatement and proof · cited by 0