instIsNontrivialOfIsNontrivialOfCompatible

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

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

← MathLib Explorer

English

If R is nontrivial and v is a compatible valuation, then v.IsNontrivial.

Русский

Если R ненулевое и валюация совместима, то v.IsNontrivial.

LaTeX

$$$v.\\mathrm{IsNontrivial}$$$

Lean4

instance {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] [IsNontrivial R] (v : Valuation R Γ₀) [v.Compatible] :
    v.IsNontrivial := by rwa [← isNontrivial_iff_isNontrivial]

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

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

Разделы

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

Аффилиация

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