toPerfPair_apply

Mathlib.LinearAlgebra.PerfectPairing.Basic

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

English

The application of the perfect pairing to a pair equals the action on the first argument.

Русский

Применение совершенной парировки к паре равняется действию на первом аргументе.

LaTeX

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

Lean4

@[simp]
theorem toPerfPair_apply (x : M) (y : N) : p.toPerfPair x y = p x y :=
  rfl

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

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

Разделы

Аффилиация

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