Theorems · Definition · commutative algebra
AddValuation
(R : Type u_3) → [Ring R] → (Γ₀ : Type u_4) → [LinearOrderedAddCommMonoidWithTop Γ₀] → Type (max u_3 u_4)
The type of Γ₀-valued additive valuations on R.
- Defined in
- Mathlib.RingTheory.Valuation.Basic
- Cited by
- 96 results in Mathlib
- Foundations
- Depth 23 from the axioms, rests on 296 definitions · uses propext, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites5
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Ringstatement and proof · cited by 7,463
- OrderDualproof · cited by 927
- Multiplicativeproof · cited by 875
- Valuationproof · cited by 823
- LinearOrderedAddCommMonoidWithTopstatement and proof · cited by 68
Cited by113
Results whose statement or proof uses this declaration.
- IsDiscreteValuationRing.addValstatement · cited by 22
- AddValuation.toValuationstatement and proof · cited by 21
- ArchimedeanClass.addValuationstatement · cited by 15
- AddValuation.IsEquivstatement and proof · cited by 8
- AddValuation.comapstatement and proof · cited by 7
- AddValuation.suppstatement and proof · cited by 7
- IsDiscreteValuationRing.addVal_uniformizerstatement · cited by 6
- AddValuation.map_mulstatement and proof · cited by 5
- AddValuation.map_powstatement and proof · cited by 5
- AddValuation.map_zerostatement and proof · cited by 5
- AddValuation.ofValuationstatement · cited by 5
- Valuation.ofAddValuationstatement · cited by 5