dualTensorHomEquivOfBasis_toLinearMap

Mathlib.LinearAlgebra.Contraction

URI: https://scilib.ai/kg/mathlib#dualTensorHomEquivOfBasis_toLinearMap

English

The dualTensorHomEquivOfBasis b is compatible with taking its toLinearMap.

Русский

Эквивалентность dualTensorHomEquivOfBasis совместима с преобразованием к линейному отображению.

LaTeX

$$$(dualTensorHomEquivOfBasis b).toLinearMap = dualTensorHom\_R M N$$$

Lean4

@[simp]
theorem dualTensorHomEquivOfBasis_toLinearMap : (dualTensorHomEquivOfBasis b).toLinearMap = dualTensorHom R M N :=
  rfl

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

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

Разделы

Аффилиация

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