Commit 2024-07-16 18:44 f0d08e65
View on Github →refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices (#9334)
Some of the concepts in LinearAlgebra/Matrix/SesquilinearForm can be generalised from Sesquilinear Forms to Sesquilinear Maps with little or no impact on the rest of Mathlib. This PR makes those generalisations.
A number of results in the ToMatrix section relating composition of maps to matrix multiplication could also be generalised, but they require a more genralised notion of matrix multiplication than we currently have available, so they are not included in the scope of this PR. Similarly for most of the results in the Det section.