Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-14 13:35 300c4395

View on Github →

feat(algebra/lie/weights): the zero root space is the Cartan subalgebra for a Noetherian Lie algebra (#14174)

Estimated changes

Modified src/algebra/lie/cartan_subalgebra.lean

added theorem lie_subalgebra.centralizer_eq_self_of_is_cartan_subalgebra

Modified src/algebra/lie/of_associative.lean

modified theorem lie_submodule.coe_map_to_endomorphism_le

added theorem lie_submodule.to_endomorphism_comp_subtype_mem

added theorem lie_submodule.to_endomorphism_restrict_eq_to_endomorphism

Modified src/algebra/lie/weights.lean

added theorem lie_algebra.is_cartan_of_zero_root_subalgebra_eq

added theorem lie_algebra.zero_root_subalgebra_eq_iff_is_cartan

added theorem lie_algebra.zero_root_subalgebra_eq_of_is_cartan

deleted theorem lie_algebra.zero_root_subalgebra_is_cartan_of_eq

added theorem lie_module.exists_pre_weight_space_zero_le_ker_of_is_noetherian

added theorem lie_module.is_nilpotent_to_endomorphism_weight_space_zero

Modified src/linear_algebra/basic.lean

added theorem linear_map.pow_apply_mem_of_forall_mem

added theorem linear_map.pow_restrict

Modified src/linear_algebra/eigenspace.lean

added theorem module.End.eigenspace_zero

added theorem module.End.generalized_eigenspace_zero