Valued.valuedCompletion_apply
theorem Valued.valuedCompletion_apply :
∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
(x : K), Valued.v (↑K x) = Valued.v x
This theorem states that for any field `K` and any type `Γ₀` which is a linear ordered commutative group with zero, if `K` is a valued field with respect to `Γ₀`, then for any element `x` of `K`, the valuation of the canonical map applied to `x` is equal to the valuation of `x`. In other words, the valuation function is preserved under the completion, and this holds for any element in the field.
More concisely: For any field `K` with a linear ordered commutative group structure `Γ₀` as its value group, and for any `x` in `K`, the valuation of `x` under the canonical map is equal to the valuation of `x` in `K` if `K` is a valued field with respect to `Γ₀`.
|
Valued.extension_extends
theorem Valued.extension_extends :
∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [hv : Valued K Γ₀]
(x : K), Valued.extension (↑K x) = Valued.v x
The theorem "Valued.extension_extends" states that for any given valued field 'K' (a field with a valuation) with valuation range of 'Γ₀' which is a linearly ordered commutative group with zero, and any element 'x' of 'K', the extension of the valuation of 'K' to its completion at 'x' is equal to the original valuation of 'x'. In simpler terms, this theorem says that extending the valuation from the field to its completion preserves the valuation of all elements in the field.
More concisely: For any valued field 'K' with linearly ordered, commutative valuation range 'Γ₀', the extension of the valuation of 'K' to its completion at any element 'x' equals the original valuation of 'x'.
|