onQuot_comap_eq — Mathlib

English

For any ideal J, the comap of the quotient valuation via onQuot equals the original valuation.

Русский

Для любого идеала J сопоставление через Quotient восстанавливает исходную оценку.

LaTeX

$$$\\forall J, (v^{\\mathrm{onQuot}}_{J}).\\mathrm{comap}(\\mathrm{Ideal.Quotient.mk}\, J) = v$$$

Lean4

@[simp]
theorem onQuot_comap_eq {J : Ideal R} (hJ : J ≤ supp v) : (v.onQuot hJ).comap (Ideal.Quotient.mk J) = v :=
  ext fun _ => rfl

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