valuation_coe — Mathlib

English

The p-adic valuation on PadicInt p matches the valuation of the corresponding element in the rational p-adics under the natural coercion.

Русский

Ценность p‑адических чисел на PadicInt p совпадает с ценностью соответствующего элемента в p‑адических числа под естественным включением.

LaTeX

$$(x : \mathbb{Q}_{p}).valuation = x.valuation$$

Lean4

@[simp, norm_cast]
theorem valuation_coe (x : ℤ_[p]) : (x : ℚ_[p]).valuation = x.valuation := by simp [valuation, valuation_coe_nonneg]

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