instIsUniformAddGroup — Mathlib

English

If 𝕜 is an AddGroup and IsUniformAddGroup, then the matrix space Matrix m n 𝕜 inherits an IsUniformAddGroup structure coordinatewise.

Русский

Если 𝕜 является аддитивной группой и IsUniformAddGroup, то пространство матриц Matrix m n 𝕜 наследует структуру IsUniformAddGroup по координатам.

LaTeX

$$$\text{IsUniformAddGroup} (Matrix\ m\ n\ 𝕜)$$$

Lean4

instance instIsUniformAddGroup [AddGroup 𝕜] [IsUniformAddGroup 𝕜] : IsUniformAddGroup (Matrix m n 𝕜) :=
  inferInstanceAs <| IsUniformAddGroup (m → n → 𝕜)

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