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.

• [x] depends on: #9475
• [ ] depends on: #13041
• [ ] depends on: #13042

[mans0954]

!bench

[leanprover-bot]

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

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

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 478890085040db180ecc9c35e252403f93333df7. There were significant changes against commit b4cd3132fe069277f225fde5e0a5ecba95b9a57f:

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

[mans0954]

File	metric	master	change	this branch
Mathlib.LinearAlgebra.Matrix.SesquilinearForm	instructions	380.472B	49.57B 13.029 %	430.042B

[mans0954]

Before:

cumulative profiling times:
        attribute application 39.8ms
        compilation 1.2s
        dsimp 0.453ms
        elaboration 2.2s
        interpretation 0.163ms
        linting 343ms
        parsing 26.6ms
        simp 3s
        tactic execution 1.23s
        type checking 1.21s
        typeclass inference 28.2s

After:

cumulative profiling times:
        attribute application 38ms
        compilation 989ms
        dsimp 0.63ms
        elaboration 2.54s
        interpretation 0.147ms
        linting 322ms
        parsing 24.5ms
        simp 2.89s
        tactic execution 1.37s
        type checking 1.15s
        typeclass inference 30.5s

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 390083a20bb91595e2baefdb18bcad0995a325a9. There were significant changes against commit b4cd3132fe069277f225fde5e0a5ecba95b9a57f:

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

[github-actions[bot]]

Import summary

No significant changes to the import graph

[github-actions[bot]]

PR summary 867eb130b7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#9475~~
• ~~leanprover-community/mathlib4#13042~~ By Dependent Issues (🤖). Happy coding!

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 7ac91b416290d11ba970ecb1f2fa15b0ff55080e. There were significant changes against commit 98151c27f6edb34c46ed3fdfa25b67c402600ba5:

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

[mans0954]

!bench

[leanprover-bot]

Here are the benchmark results for commit 6f6a726b5d6f36a678ab71c052f191d88fd44473. There were significant changes against commit 70523677f8db8e24034c887ba807ac9fc88d6103:

  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[bot]]

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

[mathlib-bors[bot]]

:v: 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[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style