Commit 2023-05-24 09:36 1976a29b

View on Github →

feat: port LinearAlgebra.Matrix.ToLinearEquiv (#3702)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Matrix/ToLinearEquiv.lean

added theorem Matrix.exists_mulVec_eq_zero_iff'

added theorem Matrix.exists_mulVec_eq_zero_iff

added theorem Matrix.exists_mulVec_eq_zero_iff_aux

added theorem Matrix.exists_vecMul_eq_zero_iff

added theorem Matrix.ker_toLin_eq_bot

added theorem Matrix.nondegenerate_iff_det_ne_zero

added theorem Matrix.range_toLin_eq_top

added def Matrix.toLinearEquiv'

added theorem Matrix.toLinearEquiv'_apply

added theorem Matrix.toLinearEquiv'_symm_apply