Commit 2026-06-11 15:25 d8bd707f

View on Github →

chore(LinearAlgebra/Matrix/Transvection): some generalizations (#40506)

Estimated changes

Modified Mathlib/LinearAlgebra/Matrix/Transvection.lean

modified theorem Matrix.mul_transvection_apply_of_ne

modified theorem Matrix.mul_transvection_apply_same

modified theorem Matrix.transvection_mul_apply_of_ne

modified theorem Matrix.transvection_mul_apply_same