strictMono

Mathlib.RingTheory.Valuation.RankOne

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

English

If v is a rank-one valuation, then the valuation homomorphism hom v is strictly increasing on Γ₀.

Русский

Если v имеет ранг один, то гомоморфная карта оценки hom v строго возрастает на Γ₀.

LaTeX

$$$\text{StrictMono}(\mathrm{hom}\,v).$$$

Lean4

theorem strictMono : StrictMono (hom v) :=
  strictMono'

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

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

Разделы

Аффилиация

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