English
Let p be prime and q,r ≠ 0 be rationals. Then the p-adic valuation is additive over multiplication: v_p(q r) = v_p(q) + v_p(r).
Русский
Пусть p — простое, и q,r ≠ 0 — рациональные числа. Тогда p-адикальная величина удовлетворяет: v_p(q r) = v_p(q) + v_p(r).
LaTeX
$$$ q \\neq 0 \\land r \\neq 0 \\Rightarrow v_p(q r) = v_p(q) + v_p(r) $$$
Lean4
/-- A rewrite lemma for `padicValRat p (q * r)` with conditions `q ≠ 0`, `r ≠ 0`. -/
protected theorem mul {q r : ℚ} (hq : q ≠ 0) (hr : r ≠ 0) : padicValRat p (q * r) = padicValRat p q + padicValRat p r :=
by
have : q * r = (q.num * r.num) /. (q.den * r.den) := by rw [Rat.mul_eq_mkRat, Rat.mkRat_eq_divInt, Nat.cast_mul]
have hq' : q.num /. q.den ≠ 0 := by rwa [Rat.num_divInt_den]
have hr' : r.num /. r.den ≠ 0 := by rwa [Rat.num_divInt_den]
have hp' : Prime (p : ℤ) := Nat.prime_iff_prime_int.1 hp.1
rw [padicValRat.defn p (mul_ne_zero hq hr) this]
conv_rhs => rw [← q.num_divInt_den, padicValRat.defn p hq', ← r.num_divInt_den, padicValRat.defn p hr']
rw [multiplicity_mul hp', multiplicity_mul hp', Nat.cast_add, Nat.cast_add]
· ring
· simp [finite_int_prime_iff]
· simp [finite_int_prime_iff, hq, hr]
