Theorem RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zero

Modification history

2025-08-11 09:25
Mathlib/LinearAlgebra/RootSystem/Base.lean
feat: roots of a root system are determined by their pairings with elements of a base (#28086) …
Added RootPairing.Base.exists_mem_support_pos_pairingIn_ne_zeroView on Github →