add_eq_max_of_ne' — Mathlib

English

The coercion from Q to Q_p preserves addition.

Русский

Встраивание из Q в Q_p сохраняет сложение.

LaTeX

$$$\\uparrow(x+y) = \\uparrow x + \\uparrow y$$$

Lean4

/-- Theorems about `padicNormE` are named with a `'` so the names do not conflict with the
equivalent theorems about `norm` (`‖ ‖`). -/
theorem add_eq_max_of_ne' {q r : ℚ_[p]} :
    padicNormE q ≠ padicNormE r → padicNormE (q + r : ℚ_[p]) = max (padicNormE q) (padicNormE r) :=
  Quotient.inductionOn₂ q r fun _ _ ↦ PadicSeq.add_eq_max_of_ne

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