ofIsMulCommutative — Mathlib

English

If a Monoid M satisfies IsMulCommutative, then M is a CommMonoid.

Русский

Если моноид M удовлетворяет условию IsMulCommutative, то M является коммутативным моноидом.

LaTeX

$$$\\\\forall M \\\\[Monoid M\\\\] \\\\forall \\\\text{inst} \\\\,[IsMulCommutative M], \\\\operatorname{CommMonoid} M, \\\\text{with } mul\\_comm$$$

Lean4

@[to_additive]
instance (priority := 100) ofIsMulCommutative {M : Type*} [Monoid M] [IsMulCommutative M] : CommMonoid M where
  mul_comm := IsMulCommutative.is_comm.comm

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