add_eq_max_of_ne — Mathlib

English

If two Padic numbers q and r have unequal norms, then ‖q + r‖ = max(‖q‖, ‖r‖).

Русский

Если два падиковых числа q и r имеют неравные нормы, то ‖q + r‖ = max(‖q‖, ‖r‖).

LaTeX

$$$\|q + r\| = \max\{\|q\|, \|r\|\}$ whenever $\|q\| \neq \|r\|$$$

Lean4

theorem add_eq_max_of_ne {q r : ℚ_[p]} (h : ‖q‖ ≠ ‖r‖) : ‖q + r‖ = max ‖q‖ ‖r‖ :=
  by
  dsimp [norm] at h ⊢
  have : padicNormE q ≠ padicNormE r := mod_cast h
  exact mod_cast padicNormE.add_eq_max_of_ne' this

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