entryLinearMap_toAddHom

Mathlib.Data.Matrix.Basic

URI: https://scilib.ai/kg/mathlib#Matrix.entryLinearMap_toAddHom

English

The AddHom obtained from entryLinearMap equals entryAddHom.

Русский

Гомоморфизм AddHom, полученный из entryLinearMap, равен entryAddHom.

LaTeX

$$entryLinearMap_toAddHom {i} {j} : (entryLinearMap R α i j : _ →+ _) = entryAddHom α i j$$

Lean4

@[simp]
theorem entryLinearMap_toAddHom {i : m} {j : n} : (entryLinearMap R α i j : AddHom _ _) = entryAddHom α i j :=
  rfl

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

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

Разделы

Аффилиация

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