Theorem RootPairing.not_isIrreducible_of_subsingleton

Modification history

2026-03-29 20:17
Mathlib/LinearAlgebra/RootSystem/Irreducible.lean
feat: order isomorphism between ideals and invariant root submodules (#37285) …
Added RootPairing.not_isIrreducible_of_subsingletonView on Github →