Commit 2023-10-08 20:38 8cdd933d

View on Github →

feat: various Lie algebra definitions / lemmas (#7507) These are all motivated by a result I've proved but I believe they make sense in their own right so I have split them out in the hopes of simplifying review.

Estimated changes

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem LieModuleEquiv.apply_eq_iff_eq_symm_apply

added theorem LieModuleEquiv.coe_coe

added theorem LieModuleEquiv.surjective

Modified Mathlib/Algebra/Lie/Nilpotent.lean

added theorem LieModule.eventually_iInf_lowerCentralSeries_eq

added theorem LieSubmodule.lcs_sup

Modified Mathlib/Algebra/Lie/OfAssociative.lean

added theorem LieModule.toEndomorphism_pow_apply_map

added theorem LieModule.toEndomorphism_pow_comp_lieHom

Modified Mathlib/Algebra/Lie/Submodule.lean

added def LieModuleEquiv.ofTop

added theorem LieModuleEquiv.ofTop_apply

added theorem LieModuleEquiv.range_coe

added theorem LieSubmodule.coe_map

added theorem LieSubmodule.comap_inf

added def LieSubmodule.mapOrderEmbedding

added theorem LieSubmodule.map_bot

added theorem LieSubmodule.map_comp

added theorem LieSubmodule.map_iSup

added theorem LieSubmodule.map_id

added theorem LieSubmodule.map_incl_le

added theorem LieSubmodule.map_incl_lt_iff_lt_top

added theorem LieSubmodule.map_incl_top

added theorem LieSubmodule.map_inf

added theorem LieSubmodule.map_inf_le

added theorem LieSubmodule.map_injective_of_injective

added theorem LieSubmodule.map_le_map_iff

added theorem LieSubmodule.map_le_range

added theorem LieSubmodule.map_mono

added theorem LieSubmodule.mem_map_of_mem

added def LieSubmodule.orderIsoMapComap

added def LieSubmodule.toSubmodule_orderEmbedding

added theorem LieSubmodule.wellFounded_of_isArtinian

Modified Mathlib/LinearAlgebra/Basic.lean

added theorem Submodule.map_inf

added theorem Submodule.map_inf_le