mul_comp — Mathlib

English

For monoid object M, and morphisms f1,f2: X → M, g: M → N, the compatible equality holds: (f1 * f2) ≫ g = (f1 ≫ g) * (f2 ≫ g).

Русский

Для моноидного объекта M и морфизмов f1,f2: X → M, g: M → N выполняется совместимость умножения: (f1 * f2) ≫ g = (f1 ≫ g) * (f2 ≫ g).

LaTeX

$$$ (f_1 * f_2) ≫ g = (f_1 ≫ g) * (f_2 ≫ g) $$$

Lean4

@[reassoc]
theorem mul_comp (f₁ f₂ : X ⟶ M) (g : M ⟶ N) [IsMonHom g] : (f₁ * f₂) ≫ g = f₁ ≫ g * f₂ ≫ g := by simp [Hom.mul_def]

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