comp_mul — Mathlib

English

Let f: X → Y and g1, g2: Y → M, where M is a monoid object. Then composing f with the product g1 * g2 equals the product of the compositions with f: f ∘ (g1 * g2) = (f ∘ g1) * (f ∘ g2).

Русский

Пусть f: X → Y и g1, g2: Y → M, где M — моноидальный объект. Тогда композиция f с произведением g1 и g2 равна произведению композиций: f ∘ (g1 · g2) = (f ∘ g1) · (f ∘ g2).

LaTeX

$$$ f \\circ (g_1 * g_2) = (f \\circ g_1) * (f \\circ g_2) $$$

Lean4

@[reassoc]
theorem comp_mul (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) : f ≫ (g₁ * g₂) = f ≫ g₁ * f ≫ g₂ :=
  ((yonedaMon.obj <| .mk M).map f.op).hom.map_mul _ _

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