factorₐ_comp — Mathlib

English

In a two-sided ideal setting with J ≤ K, the composition of factorₐ maps is equal to mkₐ for the transitive order hIJ.trans hJK.

Русский

В условиях двухсторонних идеалов, если J ≤ K, композиция factorₐ эквивалентна mkₐ для перехода по порядку hIJ.trans hJK.

LaTeX

$$$(Ideal.Quotient.factorₐ R₁ hJK).comp (Ideal.Quotient.factorₐ R₁ hIJ) = Ideal.Quotient.factorₐ R₁ (hIJ.trans hJK)$$$

Lean4

@[simp]
theorem factorₐ_comp {K : Ideal A} [K.IsTwoSided] (hJK : J ≤ K) :
    (Ideal.Quotient.factorₐ R₁ hJK).comp (Ideal.Quotient.factorₐ R₁ hIJ) = Ideal.Quotient.factorₐ R₁ (hIJ.trans hJK) :=
  Ideal.Quotient.algHom_ext _ (by ext; simp)

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