Theorems · Definition · commutative algebra
IsDiscreteValuationRing.addVal
(R : Type u) → [inst : CommRing R] → [inst_1 : IsDomain R] → [IsDiscreteValuationRing R] → AddValuation R ℕ∞
The ℕ∞-valued additive valuation on a DVR.
- Cited by
- 22 results in Mathlib
- Foundations
- Depth 88 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites6
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
- ENatstatement · cited by 4,985
- IsDomainstatement and proof · cited by 2,196
- IsDiscreteValuationRingstatement and proof · cited by 117
- AddValuationstatement · cited by 96
- multiplicity_addValuationproof · cited by 2
Cited by24
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.toWithBotNatproof · cited by 6
- IsDiscreteValuationRing.addVal_uniformizerstatement and proof · cited by 6
- IsDiscreteValuationRing.idealOrderIsoENatproof · cited by 5
- IsDiscreteValuationRing.addVal_eq_top_iffstatement and proof · cited by 4
- IsDiscreteValuationRing.addVal_eq_zero_of_unitstatement · cited by 4
- Ring.ord_eq_addValstatement and proof · cited by 3
- IsDiscreteValuationRing.addVal_defstatement · cited by 3
- IsDiscreteValuationRing.addVal_zerostatement and proof · cited by 3
- IsDiscreteValuationRing.intValuation_maximalIdealstatement and proof · cited by 3
- Ring.ordFrac_eq_inverse_comp_valuationproof · cited by 2
- IsDiscreteValuationRing.toWithBotNat_le_toWithBotNat_iffproof · cited by 1
- IsDiscreteValuationRing.addVal_addstatement and proof · cited by 1