Theorems · Theorem · commutative algebra
ValuationSubring.isMax_toLocalSubring
∀ {K : Type u_3} [inst : Field K] (R : ValuationSubring K), IsMax R.toLocalSubring[Stacks Tag 052K](https://stacks.math.columbia.edu/tag/052K)
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 58 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.
Cites24
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Fieldstatement and proof · cited by 7,404
- mul_oneproof · cited by 3,885
- IsUnitproof · cited by 1,602
- LE.le.antisymmproof · cited by 507
- Eq.geproof · cited by 375
- IsMaxstatement · cited by 372
- inv_mul_cancel₀proof · cited by 267
- ValuationSubringstatement and proof · cited by 187
- Subsemigroup.carrierproof · cited by 160
- Submonoid.toSubsemigroupproof · cited by 159
- Subsemiring.toSubmonoidproof · cited by 153
Cited by2
Results whose statement or proof uses this declaration.
- bijective_rangeRestrict_comp_of_valuationRingproof · cited by 1
- LocalSubring.isMax_iffproof · cited by 0