Commit 2024-03-20 10:53 64aa2a28

View on Github →

chore(LinearAlgebra/Matrix/ToLin): clean up (#11171)

Estimated changes

Modified Mathlib/Data/Matrix/Basic.lean

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified theorem Algebra.leftMulMatrix_injective