Theorem Submodule.disjoint_ker_of_finrank_eq

Modification history

2024-12-09 13:51

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

feat: non-degeneracy of root pairing form without assuming ordered scalars (#19767) …

Deleted Submodule.disjoint_ker_of_finrank_eq View on Github →

2024-11-20 20:34

Mathlib/LinearAlgebra/Dimension/RankNullity.lean

feat (LinearAlgebra/RootSystem/Finite): nondegeneracy of canonical bilinear form restricted to root span (#18569) …

Added Submodule.disjoint_ker_of_finrank_eq View on Github →