valuation_ratCast — Mathlib

English

For any rational q, valuation(q in ℚ_p) equals padicValRat p q.

Русский

Для любого рационального числа q, valuation(q в ℚ_p) равна padicValRat p q.

LaTeX

$$$\\mathrm{valuation}(q: \\mathbb{Q}_p) = \\mathrm{padicValRat}(p,q)$$$

Lean4

@[simp]
theorem valuation_ratCast (q : ℚ) : valuation (q : ℚ_[p]) = padicValRat p q :=
  by
  rcases eq_or_ne q 0 with rfl | hq
  · simp only [Rat.cast_zero, valuation_zero, padicValRat.zero]
  refine
    neg_injective
      ((zpow_right_strictMono₀ (mod_cast hp.out.one_lt)).injective <|
        (norm_eq_zpow_neg_valuation (mod_cast hq)).symm.trans ?_)
  rw [eq_padicNorm, ← Rat.cast_natCast, ← Rat.cast_zpow, Rat.cast_inj]
  exact padicNorm.eq_zpow_of_nonzero hq

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