Theorem RootPairing.Base.cartanMatrix_mem_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_mem_of_neView on Github →
2025-04-15 16:58
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
feat: definition + basic results for chains / strings in root pairings (#24077)
Modified RootPairing.Base.cartanMatrix_mem_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_mem_of_neView on Github →
2025-03-20 18:56
Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
feat: off-diagonal entries of Cartan matrices belong to `{-3, -2, -1, 0}` (#23077) …
Added RootPairing.Base.cartanMatrix_mem_of_neView on Github →