Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-17 06:01 739d93c6

View on Github →

feat(algebra/lie/weights): the zero root subalgebra is self-normalizing (#7622)

Estimated changes

Modified src/algebra/lie/subalgebra.lean

added theorem lie_subalgebra.mem_mk_iff

Modified src/algebra/lie/weights.lean

added theorem lie_algebra.mem_zero_root_subalgebra

added theorem lie_algebra.zero_root_subalgebra_is_cartan_of_eq

added theorem lie_algebra.zero_root_subalgebra_normalizer_eq_self

added theorem lie_module.coe_weight_space'

added def lie_module.weight_space'