Commit 2025-12-01 22:59 b07e7ab8

View on Github →

feat(LinearAlgebra/Dual/BaseChange): base change of a linear form (on the Module.Dual) (#31162) Base change map for Module.Dual.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/DirectSum/Module.lean

added theorem DirectSum.coe_congrAddEquiv

added theorem DirectSum.coe_congrLinearEquiv

deleted theorem DirectSum.coe_congr_addEquiv

deleted theorem DirectSum.coe_congr_linearEquiv

added def DirectSum.congrAddEquiv

added def DirectSum.congrLinearEquiv

added theorem DirectSum.congrLinearEquiv_toAddEquiv

added theorem DirectSum.congrLinearEquiv_toLinearMap

deleted def DirectSum.congr_addEquiv

deleted def DirectSum.congr_linearEquiv

deleted theorem DirectSum.congr_linearEquiv_toAddEquiv

deleted theorem DirectSum.congr_linearEquiv_toLinearMap

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

modified def LinearEquiv.congrLeft

Modified Mathlib/LinearAlgebra/Basis/Defs.lean

added theorem Module.Basis.constr_symm_apply

Created Mathlib/LinearAlgebra/Dual/BaseChange.lean

added theorem IsBaseChange.dual

added theorem IsBaseChange.toDualBaseChange_tmul

added theorem IsBaseChange.toDual_apply

added theorem IsBaseChange.toDual_comp_apply

added def Module.Dual.baseChange

added theorem Module.Dual.baseChange_apply_tmul

added theorem Module.Dual.baseChange_baseChange

added def Module.Dual.congr

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

added theorem LinearMap.baseChange_baseChange

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean

added theorem IsBaseChange.linearMapLeftRightHom_comp_apply

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangePi.lean