valuation_surjective — Mathlib

English

The valuation map v.valuation_K: K → ℤᵐ⁰ is surjective; every value in the value group is attained by some element of K.

Русский

Оценочная карта v.valuation_K: K → ℤᵐ⁰ сюръективна; каждая величина в группе значений достигается некоторым элементом K.

LaTeX

$$Function.Surjective (v.valuation K)$$

Lean4

theorem valuation_surjective : Function.Surjective (v.valuation K) :=
  by
  intro x
  induction x with
  | zero => simp
  | coe
    x =>
    induction x with
    | ofAdd x
    obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
    refine ⟨π ^ (-x), ?_⟩
    simp [hπ, ← WithZero.coe_zpow, ← ofAdd_zsmul]

Похожие утверждения