Commit 2024-11-07 11:59 84343c90

View on Github →

feat: define restrictions of perfect pairings (#18559) The main results are:

PerfectPairing.restrict
PerfectPairing.restrictScalars
PerfectPairing.restrictScalarsField

Estimated changes

Modified Mathlib.lean

Deleted Mathlib/Algebra/Module/Algebra.lean

deleted def LinearMap.restrictScalarsLinearMap

Modified Mathlib/Algebra/Module/Submodule/Equiv.lean

added theorem LinearEquiv.ofInjective_symm_apply

added theorem LinearMap.codRestrict₂_apply

Modified Mathlib/LinearAlgebra/BilinearMap.lean

added theorem LinearMap.restrictScalarsRange_apply

added theorem LinearMap.restrictScalarsRange_apply_eq_zero_iff

Modified Mathlib/LinearAlgebra/Dual.lean

added theorem Submodule.coe_dualAnnihilator_span

added theorem Submodule.coe_dualCoannihilator_span

Modified Mathlib/LinearAlgebra/Matrix/FiniteDimensional.lean

Modified Mathlib/LinearAlgebra/PerfectPairing.lean

added def LinearEquiv.flip

added def LinearEquiv.toPerfectPairing

added def PerfectPairing.mkOfInjective'

added def PerfectPairing.mkOfInjective

added def PerfectPairing.restrict

added def PerfectPairing.restrictScalars

added def PerfectPairing.restrictScalarsField

added def PerfectPairing.toDualLeft

added def PerfectPairing.toDualRight

Modified Mathlib/LinearAlgebra/Projection.lean

added def LinearMap.linearProjOfIsCompl

added theorem LinearMap.linearProjOfIsCompl_apply_left