comp_units_smul

Mathlib.CategoryTheory.Linear.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Linear.comp_units_smul

English

Composition with a fixed morphism respects scalar units: (f)·(r) = r·(f)·g.

Русский

Состязание композиции с единицами сохраняет линейность по скаляру.

LaTeX

$$$f\\circ (r\\cdot g) = r\\cdot(f\\circ g)$.$$

Lean4

@[simp]
theorem comp_units_smul {X Y Z : C} (f : X ⟶ Y) (r : Rˣ) (g : Y ⟶ Z) : f ≫ (r • g) = r • f ≫ g := by
  apply Linear.comp_smul

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

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

Разделы

Аффилиация

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