Def RootPairing.indexNeg

Modification history

2026-07-16 01:47
Mathlib/LinearAlgebra/RootSystem/Defs.lean
chore: bump toolchain to v4.33.0-rc1 (#41779)
Modified RootPairing.indexNegView on Github →
2026-03-10 05:56
Mathlib/LinearAlgebra/RootSystem/Defs.lean
chore: bump toolchain to v4.29.0-rc6 (#36422)
Modified RootPairing.indexNegView on Github →
2025-02-14 13:43
Mathlib/LinearAlgebra/RootSystem/Defs.lean
feat: characterise linearly dependent roots of root pairings (#21851) …
Added RootPairing.indexNegView on Github →