Theorem LieIdeal.root_apply_eq_zero_of_notMem_rootSet

Modification history

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