self_le_supp_comap — Mathlib

English

For a valuation v on R/J, the ideal J is contained in the support of the comapped valuation.

Русский

Для оценивания v на R/J, J входит в опору сопоставленного оценивания.

LaTeX

$$$J \\le (v.comap (\\mathrm{Ideal.Quotient.mk}\, J)).\\mathrm{supp}$$$

Lean4

theorem self_le_supp_comap (J : Ideal R) (v : AddValuation (R ⧸ J) Γ₀) : J ≤ (v.comap (Ideal.Quotient.mk J)).supp :=
  Valuation.self_le_supp_comap J v

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