Commit 2020-05-12 15:37 11415339

feat(data/matrix): matrix and vector notation (#2656) This PR adds notation for matrices and vectors as discussed on Zulip a couple of months ago, so that ![![a, b], ![c, d]] constructs a 2x2 matrix with rows ![a, b] : fin 2 -> α and ![c, d]. It also adds corresponding simp lemmas for all matrix operations defined in data.matrix.basic. These lemmas should apply only when the input already contains ![...]. To express the simp lemmas nicely, I defined a function dot_product : (v w : n -> α) -> α which returns the sum of the entrywise product of two vectors. IMO, this makes the definitions of matrix.mul, matrix.mul_vec and matrix.vec_mul clearer, and it allows us to share some proofs. I could also inline dot_product (restoring the old situation) if the reviewers prefer.