Theorems · Theorem · commutative algebra
LocalSubring.mem_of_isMax_of_isIntegral
∀ {K : Type u_3} [inst : Field K] {R : LocalSubring K},
IsMax R → ∀ {x : K}, IsIntegral (↥R.toSubring) x → x ∈ R.toSubring[Stacks Tag 00IC](https://stacks.math.columbia.edu/tag/00IC)
- Cited by
- 1 results in Mathlib
- Foundations
- Depth 138 from the axioms · uses propext, Classical.choice, Quot.sound
- Assumes
- Field
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites40
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Top.topproof · cited by 9,680
- SetLike.coeproof · cited by 8,199
- Fieldstatement and proof · cited by 7,404
- Set.imageproof · cited by 5,609
- Idealproof · cited by 4,748
- Algebra.algebraMapproof · cited by 4,706
- LE.le.transproof · cited by 3,151
- le_reflproof · cited by 2,061
- Subalgebraproof · cited by 1,353
- Ideal.mapproof · cited by 692
- Subringstatement · cited by 602
Cited by1
Results whose statement or proof uses this declaration.
- LocalSubring.exists_valuationRing_of_isMaxproof · cited by 2