Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-08 13:26 132328c4

View on Github →

feat(algebra/lie/weights): define weight spaces of Lie modules (#7537)

Estimated changes

Modified docs/references.bib

Modified src/algebra/lie/cartan_subalgebra.lean

Created src/algebra/lie/character.lean

added def lie_algebra.lie_character

added theorem lie_algebra.lie_character_apply_lie

added theorem lie_algebra.lie_character_apply_of_mem_derived

added def lie_algebra.lie_character_equiv_linear_dual

Modified src/algebra/lie/nilpotent.lean

deleted theorem lie_algebra.nilpotent_iff_equiv_nilpotent

added theorem lie_equiv.nilpotent_iff_equiv_nilpotent

Modified src/algebra/lie/submodule.lean

added theorem lie_submodule.mem_mk_iff

added theorem lie_submodule.nontrivial_iff

added theorem lie_submodule.subsingleton_iff

Created src/algebra/lie/weights.lean

added def lie_algebra.is_root

added def lie_algebra.root_space

added theorem lie_algebra.zero_root_space_eq_top_of_nilpotent

added theorem lie_module.coe_weight_space_of_top

added def lie_module.is_weight

added theorem lie_module.is_weight_zero_of_nilpotent

added theorem lie_module.lie_mem_pre_weight_space_of_mem_pre_weight_space

added theorem lie_module.mem_pre_weight_space

added theorem lie_module.mem_weight_space

added def lie_module.pre_weight_space

added def lie_module.weight_space

added theorem lie_module.zero_weight_space_eq_top_of_nilpotent'

added theorem lie_module.zero_weight_space_eq_top_of_nilpotent

Modified src/data/nat/basic.lean

added theorem nat.le_or_le_of_add_eq_add_pred

Modified src/linear_algebra/basic.lean

added theorem linear_map.commute_pow_left_of_commute

added theorem linear_map.pow_map_zero_of_le