Theorem LinearMap.BilinForm.ker_restrict_eq_of_codisjoint

Modification history

2024-04-12 08:07
Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
refactor(LinearAlgebra): replace Submodule.restrictBilinear by BilinForm.restrict (#12045) …
Added LinearMap.BilinForm.ker_restrict_eq_of_codisjointView on Github →