Commit 2026-06-29 19:21 35ab429f

View on Github →

feat(LinearAlgebra/SesquilinearForm): moving orthogonality to own file (#37963) Move Submodule.orthogonalBilin and all lemmas that use it from SesquilinearForm/Basic.lean to its own file SesquilinearForm/Orthogonal.lean. We also add gcongr to orthogonalBilin_le.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/InnerProductSpace/Orthogonal.lean

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

Modified Mathlib/LinearAlgebra/QuadraticForm/Basic.lean

Modified Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean

deleted theorem LinearMap.isCompl_span_singleton_orthogonal

deleted theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal

deleted theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker

deleted theorem LinearMap.span_singleton_inf_orthogonal_eq_bot

deleted theorem LinearMap.span_singleton_sup_orthogonal_eq_top

deleted theorem Submodule.le_orthogonalBilin_orthogonalBilin

deleted theorem Submodule.mem_orthogonalBilin_iff

deleted def Submodule.orthogonalBilin

deleted theorem Submodule.orthogonalBilin_le

Created Mathlib/LinearAlgebra/SesquilinearForm/Orthogonal.lean

added theorem LinearMap.isCompl_span_singleton_orthogonal

added theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal

added theorem LinearMap.orthogonal_span_singleton_eq_to_lin_ker

added theorem LinearMap.span_singleton_inf_orthogonal_eq_bot

added theorem LinearMap.span_singleton_sup_orthogonal_eq_top

added theorem Submodule.le_orthogonalBilin_orthogonalBilin

added theorem Submodule.mem_orthogonalBilin_iff

added def Submodule.orthogonalBilin

added theorem Submodule.orthogonalBilin_le