Theorems · Definition · commutative algebra
ValuationSubring.toLocalSubring
{K : Type u_3} → [inst : Field K] → ValuationSubring K → LocalSubring KCast a valuation subring to a local subring.
- Cited by
- 10 results in Mathlib
- Foundations
- Depth 57 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.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Fieldstatement and proof · cited by 7,404
- ValuationSubringstatement and proof · cited by 187
- ValuationSubring.toSubringproof · cited by 32
- LocalSubringstatement · cited by 18
Cited by10
Results whose statement or proof uses this declaration.
- ValuationSubring.isMax_toLocalSubringstatement and proof · cited by 2
- Ideal.image_subset_nonunits_valuationSubringproof · cited by 2
- LocalSubring.exists_le_valuationSubringstatement and proof · cited by 2
- LocalSubring.exists_valuationRing_of_isMaxstatement · cited by 2
- IsLocalRing.exists_factor_valuationRingproof · cited by 1
- LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedInstatement and proof · cited by 1
- bijective_rangeRestrict_comp_of_valuationRingproof · cited by 1
- LocalSubring.isMax_iffstatement and proof · cited by 0
- ValuationSubring.toLocalSubring_injectivestatement and proof · cited by 0
- LocalSubring.eq_iInf_of_isIntegrallyClosedInstatement and proof · cited by 0