pointwiseAddCommMonoid — Mathlib

English

The submodules form a commutative additive monoid under the join, i.e., S ⊞ T = S ⊔ T.

Русский

Подмодули образуют коммутативный аддитивный моноид по операции объединения.

LaTeX

$$$S \oplus T = S \sqcup T$ and this defines a commutative monoid structure$$

Lean4

instance pointwiseAddCommMonoid : AddCommMonoid (Submodule R M)
    where
  add_assoc := sup_assoc
  zero_add := bot_sup_eq
  add_zero := sup_bot_eq
  add_comm := sup_comm
  nsmul := nsmulRec

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