factor_eq

Mathlib.RingTheory.Ideal.Quotient.Defs

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

English

The composition of factors equals the factor for the composed map.

Русский

Составление факторов эквивалентно фактору от композиции.

LaTeX

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

Lean4

@[simp]
theorem factor_eq : factor (le_refl S) = RingHom.id _ := by
  ext
  simp

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

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

Разделы

Аффилиация

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