factor_comp_mk

Mathlib.RingTheory.Ideal.Quotient.Defs

URI: https://scilib.ai/kg/mathlib#Ideal.Quotient.factor_comp_mk

English

The two-step factorization equals the single factor of the composite relation.

Русский

Двухшаговая факторизация равна фактору от совокупности отношений.

LaTeX

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

Lean4

@[simp]
theorem factor_comp_mk (H : S ≤ T) : (factor H).comp (mk S) = mk T :=
  by
  ext x
  rw [RingHom.comp_apply, factor_mk]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru