valuation_mul — Mathlib

English

For nonzero x,y, v_p(xy) = v_p(x) + v_p(y).

Русский

Для ненулевых x,y выполняется v_p(xy) = v_p(x) + v_p(y).

LaTeX

$$$v_p(xy) = v_p(x) + v_p(y)\quad \text{for } x \neq 0,\ y \neq 0$$$

Lean4

@[simp]
theorem valuation_mul {x y : ℚ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) : (x * y).valuation = x.valuation + y.valuation :=
  by
  have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y
  have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one
  have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _
  rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy, norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ←
    zpow_add₀ hp_pos.ne', zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm

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