Commit 2023-06-02 13:42 a0b995b7

View on Github →

feat: port Algebra.Lie.Submodule (#3045)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Basic.lean

added theorem LieModuleHom.coe_toLinearMap

deleted theorem LieModuleHom.coe_to_linearMap

Modified Mathlib/Algebra/Lie/Subalgebra.lean

Created Mathlib/Algebra/Lie/Submodule.lean

added def LieHom.IsIdealMorphism

added def LieHom.idealRange

added theorem LieHom.idealRange_eq_lieSpan_range

added theorem LieHom.idealRange_eq_map

added theorem LieHom.idealRange_eq_top_of_surjective

added theorem LieHom.isIdealMorphism_def

added theorem LieHom.isIdealMorphism_iff

added theorem LieHom.isIdealMorphism_of_surjective

added def LieHom.ker

added theorem LieHom.ker_coeSubmodule

added theorem LieHom.ker_eq_bot

added theorem LieHom.ker_le_comap

added theorem LieHom.le_ker_iff

added theorem LieHom.map_le_idealRange

added theorem LieHom.mem_idealRange

added theorem LieHom.mem_idealRange_iff

added theorem LieHom.mem_ker

added theorem LieHom.range_coeSubmodule

added theorem LieHom.range_eq_top

added theorem LieHom.range_subset_idealRange

added theorem LieIdeal.bot_of_map_eq_bot

added theorem LieIdeal.coe_bracket_of_module

added theorem LieIdeal.coe_homOfLe

added theorem LieIdeal.coe_map_of_surjective

added theorem LieIdeal.coe_toSubalgebra

added theorem LieIdeal.coe_to_lieSubalgebra_to_submodule

added def LieIdeal.comap

added theorem LieIdeal.comap_coeSubmodule

added theorem LieIdeal.comap_incl_self

added theorem LieIdeal.comap_map_eq

added theorem LieIdeal.comap_map_le

added theorem LieIdeal.comap_mono

added theorem LieIdeal.gc_map_comap

added def LieIdeal.homOfLe

added theorem LieIdeal.homOfLe_apply

added theorem LieIdeal.homOfLe_injective

added def LieIdeal.incl

added theorem LieIdeal.incl_apply

added theorem LieIdeal.incl_coe

added theorem LieIdeal.incl_idealRange

added theorem LieIdeal.incl_isIdealMorphism

added theorem LieIdeal.incl_range

added theorem LieIdeal.ker_incl

added def LieIdeal.map

added theorem LieIdeal.map_coeSubmodule

added theorem LieIdeal.map_comap_eq

added theorem LieIdeal.map_comap_le

added theorem LieIdeal.map_eq_bot_iff

added theorem LieIdeal.map_le

added theorem LieIdeal.map_le_iff_le_comap

added theorem LieIdeal.map_mono

added theorem LieIdeal.map_of_image

added theorem LieIdeal.map_sup

added theorem LieIdeal.map_sup_ker_eq_map'

added theorem LieIdeal.map_sup_ker_eq_map

added theorem LieIdeal.mem_comap

added theorem LieIdeal.mem_map

added theorem LieIdeal.mem_map_of_surjective

added def LieIdeal.topEquiv

added theorem LieIdeal.topEquiv_apply

added theorem LieIdeal.top_coe_lieSubalgebra

added theorem LieModuleHom.coeSubmodule_range

added theorem LieModuleHom.coe_range

added theorem LieModuleHom.comp_ker_incl

added def LieModuleHom.ker

added theorem LieModuleHom.ker_coeSubmodule

added theorem LieModuleHom.ker_eq_bot

added theorem LieModuleHom.ker_id

added theorem LieModuleHom.le_ker_iff_map

added theorem LieModuleHom.map_top

added theorem LieModuleHom.mem_ker

added theorem LieModuleHom.mem_range

added def LieModuleHom.range

added theorem LieSubalgebra.coe_toLieSubmodule

added theorem LieSubalgebra.exists_lieIdeal_coe_eq_iff

added theorem LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff

added theorem LieSubalgebra.mem_toLieSubmodule

added def LieSubalgebra.toLieSubmodule

added def LieSubalgebra.topEquiv

added theorem LieSubalgebra.topEquiv_apply

added theorem LieSubmodule.add_eq_sup

added theorem LieSubmodule.bot_coe

added theorem LieSubmodule.bot_coeSubmodule

added theorem LieSubmodule.coeSubmodule_comap

added theorem LieSubmodule.coeSubmodule_injective

added theorem LieSubmodule.coeSubmodule_le_coeSubmodule

added theorem LieSubmodule.coeSubmodule_map

added theorem LieSubmodule.coe_add

added theorem LieSubmodule.coe_bracket

added theorem LieSubmodule.coe_copy

added theorem LieSubmodule.coe_homOfLe

added theorem LieSubmodule.coe_injective

added theorem LieSubmodule.coe_lieSpan_submodule_eq_iff

added theorem LieSubmodule.coe_neg

added theorem LieSubmodule.coe_smul

added theorem LieSubmodule.coe_sub

added theorem LieSubmodule.coe_toSet_mk

added theorem LieSubmodule.coe_toSubmodule

added theorem LieSubmodule.coe_toSubmodule_eq_iff

added theorem LieSubmodule.coe_toSubmodule_mk

added theorem LieSubmodule.coe_zero

added def LieSubmodule.comap

added theorem LieSubmodule.comap_incl_eq_bot

added theorem LieSubmodule.comap_incl_eq_top

added theorem LieSubmodule.comap_incl_self

added theorem LieSubmodule.copy_eq

added theorem LieSubmodule.ext

added theorem LieSubmodule.gc_map_comap

added def LieSubmodule.homOfLe

added theorem LieSubmodule.homOfLe_apply

added theorem LieSubmodule.homOfLe_injective

added def LieSubmodule.incl

added theorem LieSubmodule.incl_apply

added theorem LieSubmodule.incl_coe

added theorem LieSubmodule.incl_eq_val

added theorem LieSubmodule.inf_coe

added theorem LieSubmodule.inf_coe_toSubmodule

added theorem LieSubmodule.ker_incl

added def LieSubmodule.lieSpan

added theorem LieSubmodule.lieSpan_eq

added theorem LieSubmodule.lieSpan_eq_bot_iff

added theorem LieSubmodule.lieSpan_le

added theorem LieSubmodule.lieSpan_mono

added def LieSubmodule.map

added theorem LieSubmodule.map_le_iff_le_comap

added theorem LieSubmodule.map_sup

added theorem LieSubmodule.mem_bot

added theorem LieSubmodule.mem_carrier

added theorem LieSubmodule.mem_coe

added theorem LieSubmodule.mem_coeSubmodule

added theorem LieSubmodule.mem_comap

added theorem LieSubmodule.mem_inf

added theorem LieSubmodule.mem_lieSpan

added theorem LieSubmodule.mem_map

added theorem LieSubmodule.mem_mk_iff

added theorem LieSubmodule.mem_sup

added theorem LieSubmodule.mem_top

added theorem LieSubmodule.mk_eq_zero

added theorem LieSubmodule.nontrivial_iff

added theorem LieSubmodule.nontrivial_iff_ne_bot

added theorem LieSubmodule.range_incl

added theorem LieSubmodule.sInf_coe

added theorem LieSubmodule.sInf_coe_toSubmodule

added theorem LieSubmodule.sInf_glb

added theorem LieSubmodule.span_empty

added theorem LieSubmodule.span_iUnion

added theorem LieSubmodule.span_union

added theorem LieSubmodule.span_univ

added theorem LieSubmodule.submodule_span_le_lieSpan

added theorem LieSubmodule.subset_lieSpan

added theorem LieSubmodule.subsingleton_iff

added theorem LieSubmodule.sup_coe_toSubmodule

added theorem LieSubmodule.top_coe

added theorem LieSubmodule.top_coeSubmodule

added theorem LieSubmodule.wellFounded_of_noetherian

added structure LieSubmodule

added theorem Submodule.exists_lieSubmodule_coe_eq_iff

added def lieIdealSubalgebra

added theorem lie_mem_left

added theorem lie_mem_right

Modified Mathlib/Algebra/Module/Submodule/Basic.lean

added theorem Submodule.eta