Theorem RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmodule

Modification history

2025-05-19 15:04
Mathlib/LinearAlgebra/RootSystem/Finite/Lemmas.lean
feat: define the `sl₂` Lie subalgebra associated to a root (#24995) …
Added RootPairing.root_mem_submodule_iff_of_add_mem_invtSubmoduleView on Github →