CategoryTheory.SingleObj.comp_as_mul

theorem CategoryTheory.SingleObj.comp_as_mul : ∀ (M : Type u) [inst : Monoid M] {x y z : CategoryTheory.SingleObj M} (f : x ⟶ y) (g : y ⟶ z), CategoryTheory.CategoryStruct.comp f g = g * f

This theorem, `CategoryTheory.SingleObj.comp_as_mul`, states that for any type `M` that is a Monoid, and for any three objects `x`, `y`, and `z` in the `SingleObj` category of `M`, the composition of two morphisms `f` (from `x` to `y`) and `g` (from `y` to `z`) in this category is the same as the multiplication of `g` and `f` in the Monoid `M`. Here, the composition of morphisms is denoted by `CategoryTheory.CategoryStruct.comp f g` and the multiplication in the Monoid `M` is denoted by `g * f`. The order of multiplication is reversed compared to the order of composition due to the convention in category theory.

More concisely: In the SingleObj category of a Monoid M, the composition of morphisms f from x to y and g from y to z equals the multiplication of g and f in M, where the order of multiplication is reversed compared to the order of composition.