mul_comm' — Mathlib

English

If M is a commutative monoid object, then the inverse braiding composed with the multiplication yields the same multiplication: the multiplication is invariant under swapping the two factors.

Русский

Если M — коммутативный моноидальный объект, тогда обратное braiding после умножения даёт то же умножение: умножение инвариантно по отношению к смене факторов.

LaTeX

$$$(\beta_{M,M})^{-1} \circ \mu = \mu$$$

Lean4

@[reassoc (attr := simp, mon_tauto)]
theorem mul_comm' [IsCommMonObj M] : (β_ M M).inv ≫ μ = μ := by simp [← cancel_epi (β_ M M).hom]

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