[Merged by Bors] - refactor(LinearAlgebra/Matrix/SesquilinearForm): Sesquilinear Maps and Matrices

[mans0954]

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.

---

See also: #9312

Hopefully this will replace #8256, in part at least.

• depends on: [Merged by Bors] - refactor(LinearAlgebra) : Remove unused commutativity hypothesis #9475
• depends on: [Merged by Bors] - refactor(LinearAlgebra/BilinearMap): Left composition, bilinear over different rings #13042

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 1ad926c.
There were significant changes against commit 357e37b:

  Benchmark                                        Metric         Change
  ======================================================================
- ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm   instructions     6.1%

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6f6a726.
There were significant changes against commit 7052367:

  Benchmark                                        Metric         Change
  ======================================================================
- ~Mathlib.LinearAlgebra.Matrix.SesquilinearForm   instructions    31.4%

[mans0954]

@j-loreaux unfortunately the benchmarks look slightly worse (I'm assuming a larger percentage in red is worse?)

[j-loreaux]

That's such a small change, and only in a single file, that it's not a big deal. It could even be noise.

[MichaelStollBayreuth]

General information:

lint:                                                  +3.5755 * 10⁹ (+0.0445%)
build:                                                 +49.877 * 10⁹ (+0.0406%)

7 files got slower by at least 10⁹ instructions:

Mathlib.LinearAlgebra.Matrix.SesquilinearForm:         +35.147 * 10⁹ (+31.4%)
Mathlib.LinearAlgebra.Matrix.BilinearForm:             +3.8428 * 10⁹ (+4.73%)
Mathlib.Combinatorics.SimpleGraph.LapMatrix:           +2.9559 * 10⁹ (+12.6%)
Mathlib.LinearAlgebra.Matrix.PosDef:                   +2.1526 * 10⁹ (+4.43%)
Mathlib.LinearAlgebra.QuadraticForm.Basic:             +1.6895 * 10⁹ (+0.926%)
Mathlib.Algebra.Lie.Classical:                         +1.3773 * 10⁹ (+3.76%)
Mathlib.CategoryTheory.Category.Cat.Limit:             +1.3142 * 10⁹ (+1.38%)

2 files got slower by at least 10%:

Mathlib.LinearAlgebra.Matrix.SesquilinearForm:                        +31.4%
Mathlib.Combinatorics.SimpleGraph.LapMatrix:                          +12.6%

No file got faster by at least 10⁹ instructions.

No file got faster by at least 10%.

[j-loreaux]

Thanks @MichaelStollBayreuth I'll let someone else decide. But I'm okay with this. The other option would be to have these general versions, and then more specific ones which are abbrevs of these to help Lean with elaboration. I expect that would help, but I'm not positive without trying it.

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by j-loreaux.

[Vierkantor]

I found a few stylistic issues. Overall I think the slower build time is worth it for the increased generality.

So looks good to me with these changes, thanks!

bors d+

[mathlib-bors]

✌️ mans0954 can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[mans0954]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style