Theorem RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem

Modification history

2025-10-11 23:02
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
feat: invariant dual submodules define Lie ideals (#29979) …
Added RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMemView on Github →