toLinearMap_toPerfPair

Mathlib.LinearAlgebra.PerfectPairing.Basic

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

English

The flipped perfect pairing is itself a perfect pairing.

Русский

Перекрытая совершенная парировка сама по себе совершенная парировка.

LaTeX

$$$$ p.flip.IsPerfPair $$$$

Lean4

@[simp]
theorem toLinearMap_toPerfPair (x : M) : p.toPerfPair x = p x :=
  rfl

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

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

Разделы

Аффилиация

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