English
There is a natural monoid isomorphism between ((M ∗ N) ∗ P) and (M ∗ (N ∗ P)), expressing the associativity of the coproduct in monoids.
Русский
Существует естественный изоморфизм моноидов между ((M ∗ N) ∗ P) и (M ∗ (N ∗ P)), выражающий ассоциативность копродукта.
LaTeX
$$$ (M \\ast N) \\ast P \\cong M \\ast (N \\ast P). $$$
Lean4
/-- A multiplicative equivalence between `(M ∗ N) ∗ P` and `M ∗ (N ∗ P)`. -/
@[to_additive /-- An additive equivalence between `AddMonoid.Coprod (AddMonoid.Coprod M N) P` and
`AddMonoid.Coprod M (AddMonoid.Coprod N P)`. -/
]
def coprodAssoc : (M ∗ N) ∗ P ≃* M ∗ (N ∗ P) :=
MonoidHom.toMulEquiv (Coprod.lift (Coprod.map (.id M) inl) (inr.comp inr))
(Coprod.lift (inl.comp inl) (Coprod.map inr (.id P))) (by ext <;> rfl) (by ext <;> rfl)
