toPerfPair_flip_comp_coroot — Mathlib

English

The flipped linear map, when composed with coroot, matches the coroot' image: (P.toLinearMap.flip).toPerfPair ∘ P.coroot = P.coroot'.

Русский

Сумма свойств отображения flip совместима с корелотами: (P.toLinearMap.flip).toPerfPair ∘ P.coroot = P.coroot'.

LaTeX

$$$$ (P.toLinearMap.flip).toPerfPair \\circ P.coroot = P.coroot'. $$$$

Lean4

@[simp]
theorem toPerfPair_flip_comp_coroot : P.toLinearMap.flip.toPerfPair ∘ P.coroot = P.coroot' :=
  rfl

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