supp_quot_supp

Mathlib.RingTheory.Valuation.Quotient

URI: https://scilib.ai/kg/mathlib#AddValuation.supp_quot_supp

English

For AddValuation, the quotient valuation has support equal to the mapped support.

Русский

Для AddValuation опора кватирования равна отображению опоры по отображению.

LaTeX

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

Lean4

theorem supp_quot_supp : supp ((Valuation.onQuot v) le_rfl) = 0 :=
  Valuation.supp_quot_supp v

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

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

Разделы

Аффилиация

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