addCommGroup — Mathlib

English

The quotient M/N inherits an additive group structure from M, i.e., M/N is an abelian group under the induced addition.

Русский

Фактор-пространство M/N наследует аддитивную структуру от M, то есть является абелевой группой под индуктивным сложением.

LaTeX

$$$M/N$ is an additive abelian group.$$

Lean4

instance addCommGroup : AddCommGroup (M ⧸ N) :=
  Submodule.Quotient.addCommGroup _

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