Commit 2023-04-21 08:03 becd6984

View on Github →

feat: port LinearAlgebra.Matrix.Nondegenerate (#3564)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/Nondegenerate.lean

added theorem Matrix.Nondegenerate.eq_zero_of_ortho

added theorem Matrix.Nondegenerate.exists_not_ortho_of_ne_zero

added def Matrix.Nondegenerate

added theorem Matrix.eq_zero_of_mulVec_eq_zero

added theorem Matrix.eq_zero_of_vecMul_eq_zero

added theorem Matrix.nondegenerate_of_det_ne_zero