mul — Mathlib

English

For nonzero integers a,b, the p-adic valuation is additive under multiplication: v_p(ab) = v_p(a) + v_p(b).

Русский

Для ненулевых a,b: v_p(ab) = v_p(a) + v_p(b).

LaTeX

$$$\\forall a,b \\in \\mathbb{Z},\\ a \\neq 0 \\wedge b \\neq 0 \\Rightarrow \\operatorname{padicValInt} p (a \\cdot b) = \\operatorname{padicValInt} p a + \\operatorname{padicValInt} p b$$$

Lean4

theorem mul {a b : ℤ} (ha : a ≠ 0) (hb : b ≠ 0) : padicValInt p (a * b) = padicValInt p a + padicValInt p b :=
  by
  simp_rw [padicValInt]
  rw [Int.natAbs_mul, padicValNat.mul] <;> rwa [Int.natAbs_ne_zero]

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