evalEquiv_toLinearMap

Mathlib.LinearAlgebra.Dual.Defs

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

English

For f: M1 ≃ M2, the dual map satisfies f.dualMap g x = g (f x).

Русский

Для f: M1 ≃ M2 дуальное отображение удовлетворяет f.dualMap g x = g (f x).

LaTeX

$$$$ f.dualMap(g)(x) = g(f(x)) \\quad (f : M_1 \\simeq M_2). $$$$

Lean4

@[simp]
theorem evalEquiv_toLinearMap : evalEquiv R M = Dual.eval R M :=
  rfl

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

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

Разделы

Аффилиация

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