Commit 2026-04-14 17:36 25560be0
View on Github →feat(Analysis/InnerProductSpace): Gram matrix det ≠ 0 iff input vectors are independent (#37918) Small lemma extracted from #37295. Convenient for talking about the determinant directly without detour through Pos(Semi)def