Commit 2024-05-30 08:17 9c539b50

View on Github →

chore(LinearAlgebra/BilinearForm/Orthogonal): add missing API lemmas (#13367) Prerequisite for #13265

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

added theorem LinearMap.BilinForm.finrank_orthogonal

added theorem LinearMap.BilinForm.orthogonal_orthogonal

added theorem LinearMap.BilinForm.orthogonal_top