Commit 2025-12-08 13:23 d3a46adb

View on Github →

feat(LinearAlgebra/Transvection): base change of transvections (#31165) The base change of a transvection of a module.

Estimated changes

Modified Mathlib/LinearAlgebra/TensorProduct/Tower.lean

modified theorem LinearEquiv.coe_baseChange

Modified Mathlib/LinearAlgebra/Transvection.lean

added theorem IsBaseChange.transvection

added theorem LinearEquiv.transvection.baseChange

added theorem LinearMap.transvection.LinearEquiv.transvection.LinearMap.transvection.baseChange

Modified Mathlib/RingTheory/TensorProduct/IsBaseChangeHom.lean

added theorem IsBaseChange.linearMapLeftRightHom_comp