Mathlib Map

Theorems · Definition · commutative algebra

Valued.v

{R : Type u} →
  {inst : Ring R} →
    {Γ₀ : outParam (Type v)} → {inst_1 : LinearOrderedCommGroupWithZero Γ₀} → [self : Valued R Γ₀] → Valuation R Γ₀
Defined in
Mathlib.Topology.Algebra.Valued.ValuationTopology
Cited by
163 results in Mathlib
Foundations
Depth 2 from the axioms, rests on 8 definitions · uses no axioms
Assumes
Valued
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Valued.integer · cited by 22Valued.integerIsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers · cited by 22HeightOneSpectrum.adicCom…Valued.toNormedField · cited by 13Valued.toNormedFieldValued.valuedCompletion_apply · cited by 11Valued.valuedCompletion_a…WithVal.valueGroupEquiv · cited by 8WithVal.valueGroupEquivValued.extension · cited by 7Valued.extensionValued.mem_nhds · cited by 7Valued.mem_nhdsWithVal.valueGroupOrderIso₀ · cited by 7WithVal.valueGroupOrderIs…Valued.hasBasis_nhds_zero · cited by 6Valued.hasBasis_nhds_zeroIsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers · cited by 5HeightOneSpectrum.mem_adi…IsDedekindDomain.HeightOneSpectrum.adicCompletion.valuation · cited by 5adicCompletion.valuationValued.hasBasis_uniformity · cited by 4Valued.hasBasis_uniformityValued.isClosed_closedBall · cited by 4Valued.isClosed_closedBallRat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv · cited by 4adicCompletionIntegers.pa…Valued.extensionValuation_apply_coe · cited by 3Valued.extensionValuation…Ring · cited by 7463RingValuation · cited by 823ValuationLinearOrderedCommGroupWithZero · cited by 528LinearOrderedCommGroupWit…Valued · cited by 70ValuedValued.vCITED BYCITES

Cites4

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Cited by178

Results whose statement or proof uses this declaration.