scalarAlgHom

Mathlib.Data.Matrix.Basic

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

English

There is an algebra hom from α to Matrix n n α sending a to the scalar matrix a·I, i.e., scalar n a.

Русский

Существует алгеброгомом α → Matrix n n α, который отправляет a в скалярную матрцу a·I.

LaTeX

$$scalarAlgHom : α →ₐ[R] Matrix n n α$$

Lean4

/-- `Matrix.scalar` as an `AlgHom`. -/
def scalarAlgHom : α →ₐ[R] Matrix n n α where
  toRingHom := scalar n
  commutes' _ := rfl

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

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

Разделы

Аффилиация

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