Theorem RootPairing.invtRootSubmodule.eq_top_iff

Modification history

2026-01-24 10:53
Mathlib/LinearAlgebra/RootSystem/Irreducible.lean
feat: golf eq_top_of_invtSubmodule_ne_bot (#32974)
Added RootPairing.invtRootSubmodule.eq_top_iffView on Github →