instAddCommGroupHom — Mathlib

English

For any X,Y in Mat R, the hom-set (X ⟶ Y) naturally carries an AddCommGroup structure, coming from the matrix addition on entries.

Русский

Для любых X,Y в Mat R множество гомоморфизмов (X ⟶ Y) естественным образом является аддитивной абелевой группой за счёт сложения матриц по компонентам.

LaTeX

$$$(X \to Y) \text{ carries } \mathrm{AddCommGroup}$$$

Lean4

instance (X Y : Mat R) : AddCommGroup (X ⟶ Y) :=
  by
  change AddCommGroup (Matrix X Y R)
  infer_instance

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