mul — Mathlib

English

The p-adic norm is multiplicative: padicNorm p (q r) = padicNorm p q · padicNorm p r for all q,r ∈ ℚ.

Русский

p-адическая норма мультипликативна: padicNorm p (q r) = padicNorm p q · padicNorm p r для всех q,r ∈ ℚ.

LaTeX

$$$ padicNorm\ p\ (q r) = padicNorm\ p\ q \cdot padicNorm\ p\ r $$$

Lean4

/-- The `p`-adic norm is multiplicative. -/
@[simp]
protected theorem mul (q r : ℚ) : padicNorm p (q * r) = padicNorm p q * padicNorm p r :=
  if hq : q = 0 then by simp [hq]
  else
    if hr : r = 0 then by simp [hr]
    else by
      have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]
      simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

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