Commit 2023-04-28 05:41 fabd0235

View on Github →

feat: port LinearAlgebra.FreeModule.Finite.Matrix (#3690)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean

added theorem FiniteDimensional.finrank_linearMap

added theorem Matrix.rank_vecMulVec