Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-15 13:58 fc63bdd3

View on Github →

chore(linear_algebra/matrix/hermitian): move matrix.conj_transpose_map to the same file as matrix.transpose_map (#15297) Also restates the hypothesis using function.semiconj since that has more API and is definitionally easier to work with.

Estimated changes