instCommRing

Mathlib.NumberTheory.Padics.PadicNumbers

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

English

Ultrametric inequality holds: ∥f+g∥ ≤ max(∥f∥, ∥g∥).

Русский

Неархимедово неравенство: \|f+g\| ≤ max(\|f\|, \|g\|).

LaTeX

$$(f + g).norm ≤ \max\{f.norm, g.norm\}$$

Lean4

instance : CommRing ℚ_[p] :=
  Cauchy.commRing

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

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

Разделы

Аффилиация

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