Theorems · Definition · field theory

Valued.extension

{K : Type u_1} →
  [inst : Field K] →
    {Γ₀ : Type u_2} →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] →
        [hv : Valued K Γ₀] → UniformSpace.Completion K → (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀

The extension of the valuation of a valued field to the completion of the field.

Defined in

Mathlib.Topology.Algebra.Valued.ValuedField

Cited by

7 results in Mathlib

Foundations

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

Assumes

FieldLinearOrderedCommGroupWithZeroValued