[Merged by Bors] - chore: deprecate duplicate declaration for the scalar product as a sesquilinear form

[sgouezel]

Zulip discussion at #mathlib4 > Duplication @ 💬

---

[github-actions]

PR summary 0bf098cae7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ orthogonalBilin_innerₗ

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

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

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[vihdzp]

Getting rid of the duplication is fine, but the other name comes off as more readable to me. I thought using non-ASCII characters in declarations was generally discouraged.

[sgouezel]

innerₛₗ is the standard spelling throughout mathlib (used 10 times more than the other one). This PR is only about removing the duplication, not changing the name. This could be done later in another PR if needed, but I think a prerequisite would be to converge on a naming scheme for our whole zoo of bundled linear maps, bilinear maps, continuous linear maps and so on.

[jcommelin]

Thanks 🎉

bors d+

[mathlib-bors]

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

[sgouezel]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step