English
Let p be prime and q ≠ 0 be a rational with q = n/d for integers n,d. Then the p-adic valuation of q satisfies v_p(q) = v_p(n) − v_p(d) (the difference of the p-adic valuations of the numerator and the denominator).
Русский
Пусть p — простое число и q ≠ 0 — рациональное число, представимое как q = n/d с целыми n,d. Тогда p-адикальная величина q равна разности величин v_p(n) и v_p(d): v_p(q) = v_p(n) − v_p(d).
LaTeX
$$$ q = \\dfrac{n}{d} \\land q \\neq 0 \\Rightarrow v_p(q) = v_p(n) - v_p(d) $$$
Lean4
/-- A rewrite lemma for `padicValRat p q` when `q` is expressed in terms of `Rat.mk`. -/
protected theorem defn (p : ℕ) [hp : Fact p.Prime] {q : ℚ} {n d : ℤ} (hqz : q ≠ 0) (qdf : q = n /. d) :
padicValRat p q = multiplicity (p : ℤ) n - multiplicity (p : ℤ) d :=
by
have hd : d ≠ 0 := Rat.mk_denom_ne_zero_of_ne_zero hqz qdf
let ⟨c, hc1, hc2⟩ := Rat.num_den_mk hd qdf
rw [padicValRat.multiplicity_sub_multiplicity hp.1.ne_one hqz]
simp only [hc1, hc2]
rw [multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1), multiplicity_mul (Nat.prime_iff_prime_int.1 hp.1)]
· rw [Nat.cast_add, Nat.cast_add]
simp_rw [Int.natCast_multiplicity p q.den]
ring
· simpa [finite_int_prime_iff, hc2] using hd
· simpa [finite_int_prime_iff, hqz, hc2] using hd
