instRankOneNNRealValuation

Mathlib.Topology.Algebra.Valued.NormedValued

URI: https://scilib.ai/kg/mathlib#NormedField.instRankOneNNRealValuation

Lean4

instance {K : Type*} [NontriviallyNormedField K] [IsUltrametricDist K] : Valuation.RankOne (valuation (K := K))
    where
  hom := .id _
  strictMono' := strictMono_id
  exists_val_nontrivial :=
    (exists_one_lt_norm K).imp fun x h ↦
      by
      have h' : x ≠ 0 := norm_eq_zero.not.mp (h.gt.trans' (by simp)).ne'
      simp [valuation_apply, ← NNReal.coe_inj, h.ne', h']

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

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

Разделы

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

Аффилиация

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