factorₐ_comp_mk — Mathlib

English

The composition of quotient maps aligns with the mk maps along two ideals I ⊆ J ⊆ K, i.e., factorₐ composed with mk is mk for the transitive inclusion.

Русский

Компоновка факторного отображения согласована с mk-образованиями вдоль цепочки вложений I ⊆ J ⊆ K.

LaTeX

$$$(Ideal.Quotient.factorₐ R₁ hJK) \\circ (Ideal.Quotient.mkₐ R₁ I) = Ideal.Quotient.mkₐ R₁ J$$$

Lean4

@[simp]
theorem factorₐ_comp_mk : (Ideal.Quotient.factorₐ R₁ hIJ).comp (Ideal.Quotient.mkₐ R₁ I) = Ideal.Quotient.mkₐ R₁ J :=
  rfl

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