norm_pos_iff_valuation_pos

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#Valued.norm_pos_iff_valuation_pos

← MathLib Explorer

English

0 < ||x|| is equivalent to 0 < v(x) in the value group.

Русский

0 < ||x|| эквивалентно 0 < v(x) в группе значений.

LaTeX

$$$$ 0 < \|x\| \iff 0 < v(x). $$$$

Lean4

theorem norm_pos_iff_valuation_pos {x : L} : 0 < Valued.norm x ↔ (0 : Γ₀) < v x :=
  by
  rw [norm_def, ← NNReal.coe_zero, NNReal.coe_lt_coe, ← map_zero (RankOne.hom (v (R := L))), StrictMono.lt_iff_lt]
  exact RankOne.strictMono v

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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