Theorem RootPairing.Base.cartanMatrix_le_zero_of_ne

Modification history

2025-07-17 18:28
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
feat: add root system induction principle equivalent to connectedness of Dynkin diagram (#26965) …
Modified RootPairing.Base.cartanMatrix_le_zero_of_neView on Github →
2025-04-09 10:11
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
feat(LinearAlgebra/RootSystem): Generalize RootPairing.pairing_zero_iff (#23833) …
Modified RootPairing.Base.cartanMatrix_le_zero_of_neView on Github →
2025-02-26 10:06
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
feat: more structural lemmas about root pairings (#22213) …
Added RootPairing.Base.cartanMatrix_le_zero_of_neView on Github →