isNontrivial_of_rankOne

Mathlib.RingTheory.Valuation.RankOne

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

English

From RankOne on R we obtain IsRankLeOne R.

Русский

Из RankOne на R следует IsRankLeOne R.

LaTeX

$$$[h : (\mathrm{valuation}\;R).RankOne] \Rightarrow \mathrm{IsRankLeOne\}R$$$

Lean4

theorem isNontrivial_of_rankOne [h : (valuation R).RankOne] : ValuativeRel.IsNontrivial R :=
  (isNontrivial_iff_isNontrivial _).mpr h.toIsNontrivial

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

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

Разделы

Аффилиация

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