Commit 2025-08-19 02:03 86c1ad13

View on Github →

feat(Data/Matrix): relax some IsUnit lemmas to IsRegular (#28500) Also generalize some related results about mulVec, vecMul, and LinearIndependent, notably Matrix.vecMul_injective_iff : Function.Injective M.vecMul ↔ LinearIndependent R M.row which now needs only Semiring instead of Ring.

Estimated changes

Modified Mathlib/Data/Matrix/Defs.lean

added theorem Matrix.ext_col

added theorem Matrix.ext_row

Modified Mathlib/Data/Matrix/Mul.lean

added theorem Matrix.isLeftRegular_iff_mulVec_injective

added theorem Matrix.isRightRegular_iff_vecMul_injective

added theorem Matrix.mul_left_injective_iff_vecMul_injective

added theorem Matrix.mul_right_injective_iff_mulVec_injective

Modified Mathlib/LinearAlgebra/Matrix/ToLin.lean

modified theorem Matrix.linearIndependent_cols_of_isUnit

modified theorem Matrix.linearIndependent_rows_of_isUnit

modified theorem Matrix.mulVec_injective_iff

modified theorem Matrix.vecMul_injective_iff