commMonoid — Mathlib

Lean4
/-- If a type carries a unital magma structure that distributes over a unital binary
operation, then the magma structure is a commutative monoid. -/
@[to_additive /-- If a type carries a unital additive magma structure that distributes over a unital binary
          operation, then the additive magma structure is a commutative additive monoid. -/
    ]
abbrev commMonoid [h : MulOneClass X] (distrib : ∀ a b c d, ((a * b) <m₁> c * d) = (a <m₁> c) * b <m₁> d) :
    CommMonoid X :=
  { h with mul_comm := (mul_comm h₁ MulOneClass.isUnital distrib).comm,
    mul_assoc := (mul_assoc h₁ MulOneClass.isUnital distrib).assoc }
Похожие утверждения