PR summary c381040244

Import changes for modified files

No significant changes to the import graph

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

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

./scripts/technical-debt-metrics.sh pr_summary

I'm surprised we don't appear to need the condition:

J (r • a) = (I r) • (J a)

CC: @eric-wieser

In principle we could make a generalisation along these lines but I think we would need to be:

1. very confident that it does not degrade the experience in much, much more common situation of a sesquilinear form
2. very thorough and systematic in terms of API development

I just spent ~ 30 minutes looking over our library of results about bilinear forms / maps, sesquilinear forms and things are looking a bit unhealthy (and we even have egregious things like both https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/SesquilinearForm.html#LinearMap.Nondegenerate and https://leanprover-community.github.io/mathlib4_docs/Mathlib/LinearAlgebra/BilinearForm/Properties.html#LinearMap.BilinForm.Nondegenerate).

I don't think I would be comfortable making a generalisation along these lines until we tidied up quite a bit.

Closed in favour of #20177

I just spent ~ 30 minutes looking over our library of results about bilinear forms / maps, sesquilinear forms and things are looking a bit unhealthy

It's a while since I last looked at it, but my impression was that a lot of the results about bilinear forms, bilinear maps and sesquilinear forms were really results about sesquilinear maps. I suspect it might be hard to untangle it all.