map_mk_eq_bot_of_le — Mathlib

English

If I ≤ J are ideals in R, then the image of I under the quotient map modulo J is the zero ideal in R/J.

Русский

Если I ⊆ J — идеалы в R, то образ I при факторизации по J равен нулевому идеалу в R/J.

LaTeX

$$$ I.map(\operatorname{Quotient.mk} J) = \bot \quad\text{whenever } I \le J $$$

Lean4

theorem map_mk_eq_bot_of_le {I J : Ideal R} [J.IsTwoSided] (h : I ≤ J) : I.map (Quotient.mk J) = ⊥ :=
  by
  rw [map_eq_bot_iff_le_ker, mk_ker]
  exact h

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