Theorem RootPairing.coe_top

Modification history

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