factor_comp_apply — Mathlib

English

Let S ⊆ T ⊆ U be two-sided ideals of a ring R. Then the natural maps R/S → R/T and R/T → R/U compose to the natural map R/S → R/U corresponding to the transitive chain S ⊆ T ⊆ U.

Русский

Пусть S ⊆ T ⊆ U — двусторонние идеалы кольца R. Тогда последовательность естественных отображений R/S → R/T и R/T → R/U компонуется в естественное отображение R/S → R/U, соответствующее цепочке S ⊆ T ⊆ U.

LaTeX

$$$$(\text{factor } H2) \circ (\text{factor } H1) = \text{factor }(H1.\text{trans } H2)$$$$

Lean4

@[simp]
theorem factor_comp_apply (H1 : S ≤ T) (H2 : T ≤ U) (x : R ⧸ S) : factor H2 (factor H1 x) = factor (H1.trans H2) x :=
  by
  rw [← RingHom.comp_apply]
  simp

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