Theorem LieIdeal.restr_inf_cartan_eq_biSup_corootSubmodule

Modification history

2026-03-25 11:56
Mathlib/Algebra/Lie/Weights/IsSimple.lean
feat: decompose ideal-Cartan intersection via coroot spans (#37142) …
Added LieIdeal.restr_inf_cartan_eq_biSup_corootSubmoduleView on Github →