commMonoid — Mathlib

English

The total commutative monoid structure on Interval α coincides with the transported one from the base components.

Русский

Общая комм-монойдовая структура Interval α совпадает с переносимой из базовых компонент.

LaTeX

$$Eq Interval.commMonoid ...$$

Lean4

@[to_additive]
instance commMonoid [CommMonoid α] [PartialOrder α] [IsOrderedMonoid α] : CommMonoid (Interval α) :=
  { Interval.mulOneClass with
    mul_comm := fun _ _ => Option.map₂_comm mul_comm
    mul_assoc := fun _ _ _ => Option.map₂_assoc mul_assoc }

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