Theorem RootPairing.coe_bot

Modification history

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