Commit 2025-04-07 15:28 ec63a83c

View on Github →

chore: split file Algebra.Lie.Submodule by creating new location for all LieIdeal content (#23789)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/Algebra/Lie/Extension.lean

Created Mathlib/Algebra/Lie/Ideal.lean

added theorem LieHom.IsIdealMorphism.eq

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_eq_bot

added theorem LieHom.ker_le_comap

added theorem LieHom.ker_toSubmodule

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_eq_top

added theorem LieHom.range_subset_idealRange

added theorem LieHom.range_toSubmodule

added theorem LieIdeal.bot_of_map_eq_bot

added theorem LieIdeal.coe_bracket_of_module

added theorem LieIdeal.coe_inclusion

added theorem LieIdeal.coe_map_of_surjective

added theorem LieIdeal.coe_toLieSubalgebra

added def LieIdeal.comap

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.comap_toSubmodule

added theorem LieIdeal.gc_map_comap

added def LieIdeal.incl

added theorem LieIdeal.incl_apply

added theorem LieIdeal.incl_coe

added theorem LieIdeal.incl_idealRange

added theorem LieIdeal.incl_injective

added theorem LieIdeal.incl_isIdealMorphism

added theorem LieIdeal.incl_range

added def LieIdeal.inclusion

added theorem LieIdeal.inclusion_apply

added theorem LieIdeal.inclusion_injective

added theorem LieIdeal.ker_incl

added def LieIdeal.map

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.map_toSubmodule

added theorem LieIdeal.mem_comap

added theorem LieIdeal.mem_map

added theorem LieIdeal.mem_map_of_surjective

added def LieIdeal.toLieSubalgebra

added theorem LieIdeal.toLieSubalgebra_toSubmodule

added def LieIdeal.topEquiv

added theorem LieIdeal.topEquiv_apply

added theorem LieIdeal.top_toLieSubalgebra

added theorem LieSubalgebra.exists_lieIdeal_coe_eq_iff

added theorem LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff

added theorem lie_mem_left

added theorem lie_mem_right

Modified Mathlib/Algebra/Lie/IdealOperations.lean

Modified Mathlib/Algebra/Lie/Quotient.lean

Modified Mathlib/Algebra/Lie/Submodule.lean

deleted theorem LieHom.IsIdealMorphism.eq

deleted def LieHom.IsIdealMorphism

deleted def LieHom.idealRange

deleted theorem LieHom.idealRange_eq_lieSpan_range

deleted theorem LieHom.idealRange_eq_map

deleted theorem LieHom.idealRange_eq_top_of_surjective

deleted theorem LieHom.isIdealMorphism_def

deleted theorem LieHom.isIdealMorphism_iff

deleted theorem LieHom.isIdealMorphism_of_surjective

deleted def LieHom.ker

deleted theorem LieHom.ker_eq_bot

deleted theorem LieHom.ker_le_comap

deleted theorem LieHom.ker_toSubmodule

deleted theorem LieHom.le_ker_iff

deleted theorem LieHom.map_le_idealRange

deleted theorem LieHom.mem_idealRange

deleted theorem LieHom.mem_idealRange_iff

deleted theorem LieHom.mem_ker

deleted theorem LieHom.range_eq_top

deleted theorem LieHom.range_subset_idealRange

deleted theorem LieHom.range_toSubmodule

deleted theorem LieIdeal.bot_of_map_eq_bot

deleted theorem LieIdeal.coe_bracket_of_module

deleted theorem LieIdeal.coe_inclusion

deleted theorem LieIdeal.coe_map_of_surjective

deleted theorem LieIdeal.coe_toLieSubalgebra

deleted def LieIdeal.comap

deleted theorem LieIdeal.comap_incl_self

deleted theorem LieIdeal.comap_map_eq

deleted theorem LieIdeal.comap_map_le

deleted theorem LieIdeal.comap_mono

deleted theorem LieIdeal.comap_toSubmodule

deleted theorem LieIdeal.gc_map_comap

deleted def LieIdeal.incl

deleted theorem LieIdeal.incl_apply

deleted theorem LieIdeal.incl_coe

deleted theorem LieIdeal.incl_idealRange

deleted theorem LieIdeal.incl_injective

deleted theorem LieIdeal.incl_isIdealMorphism

deleted theorem LieIdeal.incl_range

deleted def LieIdeal.inclusion

deleted theorem LieIdeal.inclusion_apply

deleted theorem LieIdeal.inclusion_injective

deleted theorem LieIdeal.ker_incl

deleted def LieIdeal.map

deleted theorem LieIdeal.map_comap_eq

deleted theorem LieIdeal.map_comap_le

deleted theorem LieIdeal.map_eq_bot_iff

deleted theorem LieIdeal.map_le

deleted theorem LieIdeal.map_le_iff_le_comap

deleted theorem LieIdeal.map_mono

deleted theorem LieIdeal.map_of_image

deleted theorem LieIdeal.map_sup

deleted theorem LieIdeal.map_sup_ker_eq_map'

deleted theorem LieIdeal.map_sup_ker_eq_map

deleted theorem LieIdeal.map_toSubmodule

deleted theorem LieIdeal.mem_comap

deleted theorem LieIdeal.mem_map

deleted theorem LieIdeal.mem_map_of_surjective

deleted def LieIdeal.toLieSubalgebra

deleted theorem LieIdeal.toLieSubalgebra_toSubmodule

deleted def LieIdeal.topEquiv

deleted theorem LieIdeal.topEquiv_apply

deleted theorem LieIdeal.top_toLieSubalgebra

deleted theorem LieSubalgebra.exists_lieIdeal_coe_eq_iff

deleted theorem LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff

deleted theorem lie_mem_left

deleted theorem lie_mem_right