Commit 2021-05-15 14:21 3c27e2ef

View on Github →

feat(algebra/lie/weights): define product of root vectors and weight vectors (#7591) Also some related results, most notably that the zero root space is a subalgebra.

Estimated changes

Modified src/algebra/lie/abelian.lean

Modified src/algebra/lie/subalgebra.lean

added theorem lie_module_hom.coe_restrict_lie

added def lie_module_hom.restrict_lie

Modified src/algebra/lie/submodule.lean

added theorem lie_subalgebra.coe_to_lie_submodule

modified theorem lie_subalgebra.exists_lie_ideal_coe_eq_iff

added theorem lie_subalgebra.mem_to_lie_submodule

added def lie_subalgebra.to_lie_submodule

added theorem lie_submodule.coe_add

added theorem lie_submodule.coe_bracket

added theorem lie_submodule.coe_neg

added theorem lie_submodule.coe_smul

added theorem lie_submodule.coe_sub

added theorem lie_submodule.coe_zero

Modified src/algebra/lie/weights.lean

added theorem lie_algebra.coe_root_space_weight_space_product_tmul

added theorem lie_algebra.coe_zero_root_subalgebra

modified def lie_algebra.is_root

added theorem lie_algebra.le_zero_root_subalgebra

added theorem lie_algebra.lie_mem_weight_space_of_mem_weight_space

modified def lie_algebra.root_space

added def lie_algebra.root_space_product

added theorem lie_algebra.root_space_product_def

added theorem lie_algebra.root_space_product_tmul

added def lie_algebra.root_space_weight_space_product

added theorem lie_algebra.to_lie_submodule_le_root_space_zero

added def lie_algebra.zero_root_subalgebra