Theorems · Definition · commutative algebra
Valuation.integer
{R : Type u} →
{Γ₀ : Type v} → [inst : Ring R] → [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → Valuation R Γ₀ → Subring RThe ring of integers under a given valuation is the subring of elements with valuation ≤ 1.
- Defined in
- Mathlib.RingTheory.Valuation.Integers
- Cited by
- 68 results in Mathlib
- Foundations
- Depth 25 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.
- DFunLike.coeproof · cited by 62,936
- Ringstatement and proof · cited by 7,463
- Set.ofPredproof · cited by 6,101
- Valuationstatement and proof · cited by 823
- Subringstatement · cited by 602
- LinearOrderedCommGroupWithZerostatement and proof · cited by 528
Cited by81
Results whose statement or proof uses this declaration.
- Valuation.valuationSubringproof · cited by 56
- Valued.integerproof · cited by 22
- Valuation.integer.integersstatement and proof · cited by 17
- Valuation.Uniformizer.valstatement · cited by 10
- Valuation.leIdealstatement and proof · cited by 7
- Valuation.leSubmodulestatement and proof · cited by 7
- ValuationRing.mem_integer_iffstatement and proof · cited by 5
- Valuation.Uniformizer.valuation_gt_onestatement · cited by 4
- Valuation.ltIdealstatement and proof · cited by 4
- Valuation.ltSubmodulestatement and proof · cited by 4
- Valuation.Uniformizer.is_generatorstatement and proof · cited by 4
- Irreducible.maximalIdeal_pow_eq_setOfPred_le_v_coe_powstatement and proof · cited by 3