bijective_dual_eval

Mathlib.LinearAlgebra.Dual.Defs

URI: https://scilib.ai/kg/mathlib#Module.bijective_dual_eval

English

As before, dual maps respect transitivity: g.dualMap.trans f.dualMap = (f.trans g).dualMap.

Русский

Как и прежде, дуальные отображения сохраняют перестановку: g.dualMap.trans f.dualMap = (f.trans g).dualMap.

LaTeX

$$$$ g.dualMap.trans f.dualMap = (f.trans g).dualMap. $$$$

Lean4

theorem bijective_dual_eval [IsReflexive R M] : Bijective (Dual.eval R M) :=
  IsReflexive.bijective_dual_eval'

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

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

Разделы

Аффилиация

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