Commit 2023-03-30 21:32 3e068ece

View on Github →

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

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

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](https://github.com/leanprover-community/mathlib/pull/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