Perfect pairings and matrices #
The file contains results connecting perfect pairings and matrices.
Main definitions #
Matrix.toPerfectPairing: regard an invertible matrix as a perfect pairing.
def
Matrix.toPerfectPairing
{R : Type u_1}
{n : Type u_2}
[CommRing R]
[Fintype n]
[DecidableEq n]
(A : Matrix n n R)
(h : Invertible A)
:
PerfectPairing R (n → R) (n → R)
We may regard an invertible matrix as a perfect pairing.
Equations
- A.toPerfectPairing h = ((A.toLinearEquiv' h).trans (dotProductEquiv R n)).toPerfectPairing
Instances For
@[simp]
theorem
Matrix.toPerfectPairing_apply_apply
{R : Type u_1}
{n : Type u_2}
[CommRing R]
[Fintype n]
[DecidableEq n]
(A : Matrix n n R)
(h : Invertible A)
(v w : n → R)
: