Theorems · Inductive type · commutative algebra
IsDiscreteValuationRing
(R : Type u) → [inst : CommRing R] → [IsDomain R] → Prop
An integral domain is a discrete valuation ring (DVR) if it's a local PID which is not a field.
- Cited by
- 117 results in Mathlib
- Foundations
- Depth 6 from the axioms, rests on 22 definitions · uses no axioms
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
Cited by149
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.maximalIdealstatement and proof · cited by 25
- IsDiscreteValuationRing.addValstatement and proof · cited by 22
- WeierstrassCurve.HasGoodReductionstatement · cited by 10
- WeierstrassCurve.IsMinimalstatement · cited by 10
- WeierstrassCurve.HasMultiplicativeReductionstatement · cited by 9
- IsDiscreteValuationRing.exists_irreduciblestatement and proof · cited by 8
- WeierstrassCurve.HasAdditiveReductionstatement · cited by 8
- IsDiscreteValuationRing.addVal_uniformizerstatement and proof · cited by 6
- IsDiscreteValuationRing.eq_unit_mul_pow_irreduciblestatement and proof · cited by 6
- IsDiscreteValuationRing.toWithBotNatstatement and proof · cited by 6
- Irreducible.maximalIdeal_eqstatement and proof · cited by 5
- IsDiscreteValuationRing.idealOrderIsoENatstatement and proof · cited by 5