supp_eq_valuation_supp — Mathlib

English

The support of the valuation equals the support defined by the valuative relation: supp R = (valuation R).supp.

Русский

Опора валидации совпадает с опорой, определяемой валюативным отношением: supp(R) = (valuation(R)).supp.

LaTeX

$$$\\mathrm{supp}(R) = (\\mathrm{valuation}\\;R).\\mathrm{supp}$$$

Lean4

theorem supp_eq_valuation_supp : supp R = (valuation R).supp :=
  by
  ext x
  constructor
  · intro h
    simp only [supp_def, Valuation.mem_supp_iff] at h ⊢
    apply ValueGroupWithZero.sound
    · simpa
    · simp
  · intro h
    have := ValueGroupWithZero.exact h
    simpa using this.left

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