mapMatrix_id

Mathlib.Data.Matrix.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.mapMatrix_id

English

There is a compatibility between scalar action and the matrix map: (a • f).mapMatrix = a • (f.mapMatrix).

Русский

Скалярное действие совместимо с отображением матриц: (a • f).mapMatrix = a • (f.mapMatrix).

LaTeX

$$$(a \\cdot f).mapMatrix = a \\cdot (f.mapMatrix)$$$

Lean4

@[simp]
theorem mapMatrix_id : LinearMap.id.mapMatrix = (LinearMap.id : Matrix m n α →ₗ[R] _) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru