ofRankLeOneStruct

Mathlib.RingTheory.Valuation.RankOne

URI: https://scilib.ai/kg/mathlib#Valuation.RankOne.ofRankLeOneStruct

Lean4

/-- A valuative relation has a rank one valuation when it is both nontrivial
and the rank is at most one. -/
def ofRankLeOneStruct [ValuativeRel.IsNontrivial R] (e : RankLeOneStruct R) : Valuation.RankOne (valuation R)
    where
  hom := e.emb
  strictMono' := e.strictMono

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

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

Разделы

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

Аффилиация

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