factor_comp — Mathlib

English

Let S ≤ T ≤ U be ideals of a ring. Then the composition of the quotient maps factor by H1 then H2 equals the quotient by the transitive inclusion H1.trans H2; i.e., (factor H2) ∘ (factor H1) = factor (H1.trans H2).

Русский

Пусть S ≤ T ≤ U — идеалы кольца. Тогда композиция факторов через H1 и H2 равна фактору по переходному включению H1.trans H2: (factor H2) ∘ (factor H1) = factor (H1.trans H2).

LaTeX

$$$ (\text{factor } H_2) \circ (\text{factor } H_1) = \text{factor } (H_1 \operatorname{trans} H_2). $$$

Lean4

@[simp]
theorem factor_comp (H1 : S ≤ T) (H2 : T ≤ U) : (factor H2).comp (factor H1) = factor (H1.trans H2) :=
  by
  ext
  simp

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