div — Mathlib

English

The p-adic norm respects division: padicNorm p (q / r) = padicNorm p q / padicNorm p r for r ≠ 0.

Русский

p-адическая норма уважает деление: padicNorm p (q / r) = padicNorm p q / padicNorm p r при r ≠ 0.

LaTeX

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

Lean4

/-- The `p`-adic norm respects division. -/
@[simp]
protected theorem div (q r : ℚ) : padicNorm p (q / r) = padicNorm p q / padicNorm p r :=
  if hr : r = 0 then by simp [hr]
  else eq_div_of_mul_eq (padicNorm.nonzero hr) (by rw [← padicNorm.mul, div_mul_cancel₀ _ hr])

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