instAddCommMonoid — Mathlib

English

The localized module is endowed with an additive commutative monoid structure compatible with localization.

Русский

Локализованный модуль наделён структурой аддитивного коммутативного моноида, совместимой с локализацией.

LaTeX

$$$\\text{AddCommMonoid}(LocalizedModule S M)$ with addition defined via liftOn₂ and mk.$$

Lean4

instance : AddCommMonoid (LocalizedModule S M) where
  add := (· + ·)
  add_assoc := add_assoc'
  zero := 0
  zero_add := zero_add'
  add_zero := add_zero'
  nsmul := (· • ·)
  nsmul_zero := nsmul_zero'
  nsmul_succ := nsmul_succ'
  add_comm := add_comm'

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