instIsTopologicalAddGroupMatrix — Mathlib

English

The space of m×n matrices over R forms a topological additive group; i.e., addition is continuous and the structure satisfies the additive group axioms in a topological sense.

Русский

Множество матриц размерности m×n над R образует топологическую группу сложения; сложение непрерывно и структура удовлетворяет аксиомам ADD в топологическом смысле.

LaTeX

$$$\\operatorname{IsTopologicalAddGroup}(\\mathrm{M}_{m\\times n}(R)).$$$

Lean4

instance [AddGroup R] [IsTopologicalAddGroup R] : IsTopologicalAddGroup (Matrix m n R) :=
  Pi.topologicalAddGroup

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