mk_eq_valuation

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#ValuativeRel.ValueGroupWithZero.mk_eq_valuation

← MathLib Explorer

English

For a valuation v, IsNontrivial R is equivalent to v.IsNontrivial.

Русский

Для валюации v: IsNontrivial R эквивалентно v.IsNontrivial.

LaTeX

$$$\\text{IsNontrivial}(R) \\iff v.IsNontrivial$$$

Lean4

theorem mk_eq_valuation {K : Type*} [Field K] [ValuativeRel K] (x : K) (y : posSubmonoid K) :
    ValueGroupWithZero.mk x y = valuation K (x / y) := by rw [Valuation.map_div, ValueGroupWithZero.mk_eq_div]

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

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

Разделы

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

Аффилиация

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