instAddCommMonoidWithOne — Mathlib

English

If α is an AddCommMonoidWithOne, then M_n(α) carries an AddCommMonoidWithOne structure, inherited from the underlying additive commutative monoid structure on α.

Русский

Если α является AddCommMonoidWithOne, то M_n(α) приобретает структуру AddCommMonoidWithOne, наследуемую от коммутативной полугруппы сложения над α.

LaTeX

$$$M_n(\alpha) \text{ is an } AddCommMonoidWithOne \text{, inherited from } α.$$$

Lean4

instance instAddCommMonoidWithOne [AddCommMonoidWithOne α] : AddCommMonoidWithOne (Matrix n n α)
    where
  __ := addCommMonoid
  __ := instAddMonoidWithOne

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