valuation_def

Mathlib.NumberTheory.Padics.Complex

URI: https://scilib.ai/kg/mathlib#PadicAlgCl.valuation_def

English

The valuation on PadicAlgCl p evaluated at x equals the NNReal norm of x: Valued.v x = ||x||_+.

Русский

Оценка на PadicAlgCl p в x равна NNReal-норме x: v(x) = ||x||_+.

LaTeX

$$$$\operatorname{Valued.v}(x)=\|x\|_+.$$$$

Lean4

/-- The valuation of `x : PadicAlgCl p` agrees with its `ℝ≥0`-valued norm. -/
theorem valuation_def (x : PadicAlgCl p) : Valued.v x = ‖x‖₊ :=
  rfl

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

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

Разделы

Аффилиация

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