Commit 2023-08-02 07:30 e6733ece

View on Github →

feat: define reflexive modules and prove basics of perfect pairings (#4989)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/LinearAlgebra/Dual.lean

deleted def Basis.evalEquiv

deleted theorem Basis.evalEquiv_toLinearMap

added theorem Module.apply_evalEquiv_symm_apply

added theorem Module.bijective_dual_eval

modified def Module.evalEquiv

added theorem Module.evalEquiv_apply

modified theorem Module.evalEquiv_toLinearMap

modified def Module.mapEvalEquiv

modified theorem Module.mapEvalEquiv_apply

modified theorem Module.mapEvalEquiv_symm_apply

added theorem Module.symm_dualMap_evalEquiv

Created Mathlib/LinearAlgebra/PerfectPairing.lean

added theorem LinearEquiv.coe_toLinearMap_flip

added theorem LinearEquiv.flip_apply

added theorem LinearEquiv.flip_flip

added theorem LinearEquiv.isReflexive_of_equiv_dual_of_isReflexive

added theorem LinearEquiv.symm_flip

added theorem LinearEquiv.trans_dualMap_symm_flip