Theorems · Definition · commutative algebra

Valuation.Completion

{Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] → {R : Type u_3} → [inst_1 : Ring R] → Valuation R Γ₀ → Type u_3

The completion of a field with respect to a valuation.

Defined in

Mathlib.Topology.Algebra.Valued.WithVal

Cited by

33 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

LinearOrderedCommGroupWithZeroRing