supp_quot_supp — Mathlib

English

The quotient valuation has support equal to the mapped support of the original valuation, when mapped via the quotient map.

Русский

Опора кватирования равна отображению опоры исходной оценки через тождественную факторизацию.

LaTeX

$$$\\mathrm{sup}(v^{\\mathrm{onQuot}}) = (\\mathrm{sup} v).map (\\mathrm{Ideal.Quotient.mk}\, J).$$$

Lean4

theorem supp_quot_supp : supp (v.onQuot le_rfl) = 0 :=
  by
  rw [supp_quot]
  exact Ideal.map_quotient_self _

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