mathlib3

3e068ece - refactor(data/matrix/basic): work around leanprover/lean4#2042 (#18696)

refactor(data/matrix/basic): work around leanprover/lean4#2042 (#18696) This adjust definitions such that everything is well-behaved in the case that things are unfolded. For each such definition, a lemma is added that replaces the equation lemma. Before this PR, we used ```lean def transpose (M : matrix m n α) : matrix n m α | x y := M y x ``` which has the nice behavior (in Lean 3 only) of `rw transpose` only unfolding the definition when it is of the applied form `transpose M i j`. If `dunfold transpose` is used then it becomes the undesirable `λ x y, M y x` in both Lean versions. After this PR, we use ```lean def transpose (M : matrix m n α) : matrix n m α := of $ λ x y, M y x -- TODO: set as an equation lemma for `transpose`, see mathlib4#3024 @[simp] lemma transpose_apply (M : matrix m n α) (i j) : transpose M i j = M j i := rfl ``` This no longer has the nice `rw` behavior, but we can't have that in Lean4 anyway (leanprover/lean4#2042). It also makes `dunfold` insert the `of`, which is better for type-safety. This affects * `matrix.transpose` * `matrix.row` * `matrix.col` * `matrix.diagonal` * `matrix.vec_mul_vec` * `matrix.block_diagonal` * `matrix.block_diagonal'` * `matrix.hadamard` * `matrix.kronecker_map` * `pequiv.to_matrix` * `matrix.circulant` * `matrix.mv_polynomial_X` * `algebra.trace_matrix` * `algebra.embeddings_matrix` While this just adds `_apply` noise in Lean 3, it is necessary when porting to Lean 4 as there the equation lemma is not generated in the way that we want. This is hopefully exhaustive; it was found by looking for lines ending in `matrix .*` followed by a `|` line