Commit 2026-06-17 06:16 8390fffb

chore(LinearAlgebra/SesquilinearForm): deprecate IsOrtho and associated lemmas (#37381) Next steps in cleaning up bilinearity and orthogonality:

• deprecate IsOrtho and accompanying trivial lemmas (this also allows to shorten the proofs in orthogonalBilin).
• deprecate ortho_smul_right and ortho_smul_left since now provable from simp.
• remove uses of deprecated definitions.
• replace IsOrtho in undergrad.yaml by iIsOrtho. See discussion at #mathlib4 > Reorganizing bilinearity and orthogonality? Due to too agressive simplification I had to remove simp from
• QuadraticMap.associated_apply
• QuadraticMap.isOrtho_polarBilin