Theorem LinearMap.transvection.LinearEquiv.transvection.coe_toLinearMap

Modification history

2025-12-22 19:35

Mathlib/LinearAlgebra/Transvection.lean

feat(LinearAlgebra/Transvection): auxiliary lemmas to compute the determinant of transvection in a module (#31138) …

Modified LinearMap.transvection.LinearEquiv.transvection.coe_toLinearMap View on Github →

2025-11-10 10:22

Mathlib/LinearAlgebra/Transvection.lean

feat(LinearAlgebra/Transvection): transvections in a module (#31164) …

Added LinearMap.transvection.LinearEquiv.transvection.coe_toLinearMap View on Github →