Commit 2024-05-30 18:12 601da139

View on Github →

chore(LinearAlgebra): fix names, add lemma on orthogonal spaces (#13384)

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

modified theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal

added theorem LinearMap.BilinForm.isCompl_orthogonal_iff_disjoint

deleted theorem LinearMap.BilinForm.nondegenerateRestrictOfDisjointOrthogonal

added theorem LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal

deleted theorem LinearMap.BilinForm.restrictOrthogonalSpanSingletonNondegenerate

added theorem LinearMap.BilinForm.restrict_nondegenerate_orthogonal_spanSingleton

Modified Mathlib/LinearAlgebra/SesquilinearForm.lean

deleted theorem LinearMap.nondegenerateRestrictOfDisjointOrthogonal

added theorem LinearMap.nondegenerate_restrict_of_disjoint_orthogonal