Commit 2026-08-18 20:21 a7c76866

View on Github →

feat(LinearAlgebra/SesquilinearForm): adding orthogonality lemmas (#40746) Add the features proposed in #34007 to align with PointedCone.dual. Other noteworthy changes:

  • rename mem_orthogonalBilin_iff to mem_orthogonaBilin to align the API with PointedCone.mem_dual.
  • generalize orthogonal_span_singleton_eq_to_lin_ker, and rename to orthogonalBilin_span_singleton.
  • rename le_orthogonalBilin_orthogonalBilin to IsRefl.le_orthogonalBilin_orthogonalBilin in order to free the name for a new version that does not assume IsRefl.

Estimated changes