Theorem Submodule.orthogonalBilin_sup_orthogonalBilin_le_orthogonalBilin_inf

Modification history

2026-08-18 20:21
Mathlib/LinearAlgebra/SesquilinearForm/Orthogonal.lean
feat(LinearAlgebra/SesquilinearForm): adding orthogonality lemmas (#40746) …
Added Submodule.orthogonalBilin_sup_orthogonalBilin_le_orthogonalBilin_infView on Github →