Theorems · Definition · commutative algebra
LocalSubring.toSubring
{R : Type u_1} → [inst : CommRing R] → LocalSubring R → Subring RThe underlying subring of a local subring.
- Cited by
- 18 results in Mathlib
- Foundations
- Depth 12 from the axioms · uses no axioms
- Assumes
- CommRing
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommRingstatement and proof · cited by 17,173
- Subringstatement · cited by 602
- LocalSubringstatement and proof · cited by 18
Cited by21
Results whose statement or proof uses this declaration.
- LocalSubring.le_ofPrimestatement · cited by 3
- ValuationSubring.isMax_toLocalSubringproof · cited by 2
- Ideal.image_subset_nonunits_valuationSubringproof · cited by 2
- LocalSubring.exists_le_valuationSubringproof · cited by 2
- LocalSubring.exists_valuationRing_of_isMaxproof · cited by 2
- LocalSubring.mapproof · cited by 1
- LocalSubring.map_maximalIdeal_eq_top_of_isMaxstatement and proof · cited by 1
- LocalSubring.mem_of_isMax_of_isIntegralstatement and proof · cited by 1
- LocalSubring.toSubring_injectivestatement and proof · cited by 1
- LocalSubring.toSubring_monostatement · cited by 1
- bijective_rangeRestrict_comp_of_valuationRingproof · cited by 1
- LocalSubring.exists_le_valuationSubring_of_isIntegrallyClosedInstatement and proof · cited by 1