supp

Mathlib.RingTheory.Valuation.Basic

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

Lean4

/-- The support of a valuation `v : R → Γ₀` is the ideal of `R` where `v` vanishes. -/
def supp : Ideal R where
  carrier := {x | v x = 0}
  zero_mem' := map_zero v
  add_mem' {x y} hx
    hy :=
    le_zero_iff.mp <|
      calc
        v (x + y) ≤ max (v x) (v y) := v.map_add x y
        _ ≤ 0 := max_le (le_zero_iff.mpr hx) (le_zero_iff.mpr hy)
  smul_mem' c x
    hx :=
    calc
      v (c * x) = v c * v x := map_mul v c x
      _ = v c * 0 := (congr_arg _ hx)
      _ = 0 := mul_zero _

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

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

Разделы

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

Аффилиация

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