Theorem RootPairing.Base.support_nonempty

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.support_nonemptyView on Github →