English
The p-adic valuation on integers is the pullback of the p-adic valuation on rationals along the natural embedding ℤ → ℚ.
Русский
p-адическая оценка на целых является вытяжкой p-адической оценки на рациональные через вложение ℤ → ℚ.
LaTeX
$$v_p^{ℤ} = (v_p^{ℚ}) \\circ (\\iota: ℤ \\hookrightarrow ℚ)$$
Lean4
theorem surjective_padicValuation (p : ℕ) [hp : Fact (p.Prime)] : Function.Surjective (Rat.padicValuation p) :=
by
intro x
induction x with
| zero => simp
| coe
x =>
induction x with
| ofAdd x
simp_rw [Rat.padicValuation, WithZero.exp, Valuation.coe_mk, MonoidWithZeroHom.coe_mk]
rcases le_or_gt 0 x with (hx | hx)
· exact ⟨(p ^ x.natAbs)⁻¹, by simp [hp.out.ne_zero, hx]⟩
· exact ⟨p ^ x.natAbs, by simp [hp.out.ne_zero, padicValRat.pow, abs_eq_neg_self.2 hx.le]⟩
