valuedAdicCompletion_surjective — Mathlib

English

The valuation map on the adic completion is surjective, by transporting surjectivity from the base valuation.

Русский

Оценочная карта на завершении по адической норме сюръективна, за счёт переноса сюръективности из базовой оценки.

LaTeX

$$Valued.valuedCompletion_surjective_iff (v.valuation K)$$

Lean4

theorem valuedAdicCompletion_surjective : Function.Surjective (Valued.v : (v.adicCompletion K) → ℤᵐ⁰) :=
  Valued.valuedCompletion_surjective_iff.mpr (v.valuation_surjective K)

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