apply_posSubmonoid_pos

Mathlib.RingTheory.Valuation.ValuativeRel.Basic

URI: https://scilib.ai/kg/mathlib#Valuation.apply_posSubmonoid_pos

← MathLib Explorer

English

For x in posSubmonoid R, valuation R x ≠ 0.

Русский

Для x внутри posSubmonoid R, valuation R x ≠ 0.

LaTeX

$$valuation(R, x) ≠ 0 for x ∈ posSubmonoid(R)$$

Lean4

@[simp]
theorem _root_.Valuation.apply_posSubmonoid_pos {Γ : Type*} [LinearOrderedCommMonoidWithZero Γ] (v : Valuation R Γ)
    [v.Compatible] (x : posSubmonoid R) : 0 < v x :=
  zero_lt_iff.mpr <| v.apply_posSubmonoid_ne_zero x

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

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

Разделы

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

Аффилиация

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