Commit 2026-02-23 17:11 9359f90e

View on Github →

feat(LinearAlgebra/BilinearForm): remove BilinForm.IsRefl hypothesis in some theorems (#34998) Strengthen some theorems in LinearAlgebra.BilinearForm.Orthogonal by removing their BilinForm.IsRefl hypothesis; they are true verbatim without it.

Estimated changes

Modified Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean

added theorem LinearMap.BilinForm.finrank_add_finrank_orthogonal'

modified theorem LinearMap.BilinForm.finrank_orthogonal

modified theorem LinearMap.BilinForm.orthogonal_top_eq_bot

added theorem LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker