addCommMonoid — Mathlib

English

The nonnegative subtype inherits a commutative additive monoid structure; addition is commutative.

Русский

Подтип неотрицательных элементов наследует коммутативный аддитивный моноид; сложение коммутативно.

LaTeX

$$$ (a, ha) + (b, hb) = (b, hb) + (a, ha) $$$

Lean4

instance addCommMonoid : AddCommMonoid { x : α // 0 ≤ x } :=
  Subtype.coe_injective.addCommMonoid _ Nonneg.coe_zero (fun _ _ => rfl) (fun _ _ => rfl)

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