comp_div

Mathlib.CategoryTheory.Monoidal.Cartesian.Grp_

URI: https://scilib.ai/kg/mathlib#GrpObj.comp_div

English

Composition distributes over division in the opposite direction: f ≫ (g/h) = (f≫g)/(f≫h).

Русский

Композиция распределяет деление в обратном направлении: f ≫ (g/h) = (f≫g)/(f≫h).

LaTeX

$$$(f \circ (g/h)) = (f \circ g) / (f \circ h)$$$

Lean4

@[reassoc]
theorem comp_div (f : X ⟶ Y) (g h : Y ⟶ G) : f ≫ (g / h) = f ≫ g / f ≫ h :=
  ((yonedaGrp.obj ⟨G⟩).map f.op).hom.map_div g h

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

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

Разделы

Аффилиация

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