Theorem RootPairing.linearIndependent_of_sub_mem_range_root'

Modification history

2025-05-06 14:17
Mathlib/LinearAlgebra/RootSystem/Reduced.lean
feat: add Geck's final root system lemma for implementing Lusztig construction (#24263) …
Added RootPairing.linearIndependent_of_sub_mem_range_root'View on Github →