Mathlib Changelog
v4
Changelog
About
Github
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