Commit 2025-04-10 10:51 8c16e6e1

feat(Matrix): row and column functions (#22957) For A : Matrix m n R and i : m, j : n, we define A.row i to refer to the ith row of A as a vector in n -> R, and A.col j to refer to the jth column of A as a vector in m -> R. A.row and A.col are defeq to A and A.transpose respectively, but are helpful to refer to these objects explicitly, avoiding noisy eta-expansions and the simplifier manipulating transposes, such as in expressions like Injective A.col. The current version has Matrix.row and Matrix.col as defs rather than abbrevs - this allows the simplifier to make the reasonable changes A.row i j -> A i j and A.col i j -> A j i, but requires some fixes to a few rws in proofs that exploit the defeq between a matrix and a function. A less aggressive version could have both as abbrevs. We also change some spellings to use the new notation (eg Set.range (fun i => A.transpose i) -> Set.range A.col). Zulip discussion