Commit 2023-12-05 15:20 0ea58036

View on Github →

feat: lemmas about perfect pairings and dual (co)annihilators (#8824)

Estimated changes

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

modified theorem LinearEquiv.symm_flip

modified theorem LinearEquiv.trans_dualMap_symm_flip

added theorem Submodule.dualAnnihilator_map_linearEquiv_flip_symm

added theorem Submodule.dualCoannihilator_map_linearEquiv_flip

added theorem Submodule.map_dualAnnihilator_linearEquiv_flip_symm

added theorem Submodule.map_dualCoannihilator_linearEquiv_flip