Commit 2023-06-22 14:11 e172d9e3

View on Github →

feat: port Data.Matrix.Invertible (#5366)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Matrix/Invertible.lean

added def Invertible.matrixMul

added def Invertible.matrixMulLeft

added def Invertible.matrixMulRight

Modified Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean