Commit 2024-04-28 11:19 6090a1f6

View on Github →

feat (LinearAlgebra/PerfectPairing) : Modules in a perfect pairing are reflexive (#12300) This PR defines the linear equivalences with dual modules given by a perfect pairing, and shows that the modules are reflexive.

Estimated changes

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

added theorem PerfectPairing.apply_apply_toDualRight_symm

added theorem PerfectPairing.apply_toDualLeft_symm_apply

added theorem PerfectPairing.bijective_toDualRight_symm_toDualLeft

added theorem PerfectPairing.reflexive_left

added theorem PerfectPairing.reflexive_right

added theorem PerfectPairing.toDualLeft_apply

added theorem PerfectPairing.toDualLeft_of_toDualRight_symm

added theorem PerfectPairing.toDualRight_apply

added theorem PerfectPairing.toDualRight_symm_comp_toDualLeft

added theorem PerfectPairing.toDualRight_symm_toDualLeft