Theorem LinearMap.ker_restrictBilinear_eq_of_codisjoint

Modification history

2024-04-12 08:07

Mathlib/Algebra/Module/Submodule/Bilinear.lean

refactor(LinearAlgebra): replace Submodule.restrictBilinear by BilinForm.restrict (#12045) …

Deleted LinearMap.ker_restrictBilinear_eq_of_codisjoint View on Github →

2023-10-13 13:56

Mathlib/Algebra/Module/Submodule/Bilinear.lean

feat: a non-singular Killing form remains non-singular when restricted to a Cartan subalgebra (#7613) …

Added LinearMap.ker_restrictBilinear_eq_of_codisjoint View on Github →