nonarchimedean

Mathlib.NumberTheory.Padics.PadicIntegers

URI: https://scilib.ai/kg/mathlib#PadicInt.nonarchimedean

English

The norm on Z_p is non-archimedean: for any q,r in Z_p, ||q + r|| ≤ max(||q||, ||r||).

Русский

Норма на Z_p неархимедова: для любых q,r ∈ Z_p выполняется ||q + r|| ≤ max(||q||, ||r||).

LaTeX

$$$$\|q + r\| \le \max\{\|q\|, \|r\|\}.$$$$

Lean4

theorem nonarchimedean (q r : ℤ_[p]) : ‖q + r‖ ≤ max ‖q‖ ‖r‖ :=
  Padic.nonarchimedean _ _

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru