apply_symm_toPerfPair_self

Mathlib.LinearAlgebra.PerfectPairing.Basic

URI: https://scilib.ai/kg/mathlib#LinearMap.apply_symm_toPerfPair_self

English

Relates the two views of applying the perfect pairing to elements.

Русский

Связь между двумя представлениями применения совершенной парировки к элементам.

LaTeX

$$$$ p.{\\rm toPerfPair} x y = p x y $$$$

Lean4

@[simp]
theorem apply_symm_toPerfPair_self (f : Dual R N) : p (p.toPerfPair.symm f) = f :=
  p.toPerfPair.apply_symm_apply f

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

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

Разделы

Аффилиация

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