isRankLeOne_of_rankOne

Mathlib.RingTheory.Valuation.RankOne

URI: https://scilib.ai/kg/mathlib#ValuativeRel.isRankLeOne_of_rankOne

English

If there exists a rank-one valuation structure on R with ValuativeRel, then ValuativeRel.IsNontrivial R.

Русский

Если существует структураRankOne оценки на R с ValuativeRel, то ValuativeRel.IsNontrivial R.

LaTeX

$$$[\mathrm{RankOne}] \Rightarrow \mathrm{ValuativeRel.IsNontrivial\}R$$$

Lean4

theorem isRankLeOne_of_rankOne [h : (valuation R).RankOne] : IsRankLeOne R :=
  ⟨⟨h.rankLeOneStruct⟩⟩

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

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

Разделы

Аффилиация

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