nonarchimedean

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

An instance of a distance on Padic p: dist(x,y) := |x − y|_p.

Русский

Экземпляр расстояния на Padic p: dist(x,y) := |x − y|_p.

LaTeX

$$dist: (x,y) ↦ |x - y|_p$$

Lean4

theorem nonarchimedean (q r : ℚ_[p]) : ‖q + r‖ ≤ max ‖q‖ ‖r‖ :=
  by
  dsimp [norm]
  exact mod_cast padicNormE.nonarchimedean' _ _

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

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

Разделы

Аффилиация

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