Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-11 09:21 97a56e63

View on Github →

refactor(algebra/lie/basic): split giant file into pieces (#6141)

Estimated changes

Created src/algebra/lie/abelian.lean

added theorem commutative_ring_iff_abelian_lie_ring

added theorem function.injective.is_lie_abelian

added theorem function.surjective.is_lie_abelian

added def is_lie_abelian

added theorem lie_abelian_iff_equiv_lie_abelian

added theorem lie_algebra.abelian_of_le_center

added def lie_algebra.center

added theorem lie_algebra.center_eq_adjoint_kernel

added theorem lie_algebra.is_lie_abelian_bot

added theorem lie_algebra.is_lie_abelian_iff_center_eq_top

added theorem lie_module.is_trivial_iff_maximal_trivial_eq_top

added def lie_module.maximal_trivial_submodule

added theorem lie_module.mem_maximal_trivial_submodule

added theorem lie_module.trivial_iff_le_maximal_trivial

added theorem lie_submodule.lie_abelian_iff_lie_self_eq_bot

added theorem lie_submodule.trivial_lie_oper_zero

added theorem trivial_lie_zero

Modified src/algebra/lie/basic.lean

deleted def alg_equiv.to_lie_equiv

deleted theorem alg_equiv.to_lie_equiv_apply

deleted theorem alg_equiv.to_lie_equiv_symm_apply

deleted theorem commutative_ring_iff_abelian_lie_ring

deleted theorem function.injective.is_lie_abelian

deleted theorem function.surjective.is_lie_abelian

deleted def is_lie_abelian

deleted theorem lie_abelian_iff_equiv_lie_abelian

deleted theorem lie_algebra.abelian_derived_abelian_of_ideal

deleted theorem lie_algebra.abelian_iff_derived_one_eq_bot

deleted theorem lie_algebra.abelian_iff_derived_succ_eq_bot

deleted theorem lie_algebra.abelian_of_le_center

deleted theorem lie_algebra.abelian_of_solvable_ideal_eq_bot_iff

deleted theorem lie_algebra.abelian_radical_iff_solvable_is_abelian

deleted theorem lie_algebra.abelian_radical_of_semisimple

deleted def lie_algebra.ad

deleted theorem lie_algebra.ad_apply

deleted def lie_algebra.center

deleted theorem lie_algebra.center_eq_adjoint_kernel

deleted theorem lie_algebra.center_eq_bot_of_semisimple

deleted theorem lie_algebra.center_le_radical

deleted theorem lie_algebra.derived_length_eq_derived_length_of_ideal

deleted theorem lie_algebra.derived_length_zero

deleted def lie_algebra.derived_series

deleted theorem lie_algebra.derived_series_def

deleted theorem lie_algebra.derived_series_of_bot_eq_bot

deleted theorem lie_algebra.derived_series_of_derived_length_succ

deleted def lie_algebra.derived_series_of_ideal

deleted theorem lie_algebra.derived_series_of_ideal_add

deleted theorem lie_algebra.derived_series_of_ideal_add_le_add

deleted theorem lie_algebra.derived_series_of_ideal_antimono

deleted theorem lie_algebra.derived_series_of_ideal_le

deleted theorem lie_algebra.derived_series_of_ideal_le_self

deleted theorem lie_algebra.derived_series_of_ideal_mono

deleted theorem lie_algebra.derived_series_of_ideal_succ

deleted theorem lie_algebra.derived_series_of_ideal_succ_le

deleted theorem lie_algebra.derived_series_of_ideal_zero

deleted def lie_algebra.equiv.of_eq

deleted theorem lie_algebra.equiv.of_eq_apply

deleted theorem lie_algebra.equiv.of_injective_apply

deleted def lie_algebra.equiv.of_subalgebra

deleted theorem lie_algebra.equiv.of_subalgebra_apply

deleted def lie_algebra.equiv.of_subalgebras

deleted theorem lie_algebra.equiv.of_subalgebras_apply

deleted theorem lie_algebra.equiv.of_subalgebras_symm_apply

deleted theorem lie_algebra.is_lie_abelian_bot

deleted theorem lie_algebra.is_lie_abelian_iff_center_eq_top

deleted theorem lie_algebra.is_semisimple_iff_no_abelian_ideals

deleted theorem lie_algebra.is_semisimple_iff_no_solvable_ideals

deleted theorem lie_algebra.is_solvable_of_injective

deleted theorem lie_algebra.le_solvable_ideal_solvable

deleted theorem lie_algebra.lie_ideal.solvable_iff_le_radical

deleted def lie_algebra.morphism.ideal_range

deleted def lie_algebra.morphism.is_ideal_morphism

deleted theorem lie_algebra.morphism.is_ideal_morphism_def

deleted def lie_algebra.morphism.ker

deleted theorem lie_algebra.morphism.ker_coe_submodule

deleted theorem lie_algebra.morphism.ker_eq_bot

deleted theorem lie_algebra.morphism.ker_le_comap

deleted theorem lie_algebra.morphism.le_ker_iff

deleted theorem lie_algebra.morphism.map_bot_iff

deleted theorem lie_algebra.morphism.map_le_ideal_range

deleted theorem lie_algebra.morphism.mem_ideal_range

deleted theorem lie_algebra.morphism.mem_ideal_range_iff

deleted theorem lie_algebra.morphism.mem_ker

deleted def lie_algebra.morphism.range

deleted theorem lie_algebra.morphism.range_bracket

deleted theorem lie_algebra.morphism.range_coe

deleted theorem lie_algebra.morphism.range_subset_ideal_range

deleted def lie_algebra.of_associative_algebra_hom

deleted theorem lie_algebra.of_associative_algebra_hom_apply

deleted theorem lie_algebra.of_associative_algebra_hom_comp

deleted theorem lie_algebra.of_associative_algebra_hom_id

deleted def lie_algebra.radical

deleted theorem lie_algebra.subsingleton_of_semisimple_lie_abelian

deleted def lie_algebra.top_equiv_self

deleted theorem lie_algebra.top_equiv_self_apply

deleted def lie_equiv_matrix'

deleted theorem lie_equiv_matrix'_apply

deleted theorem lie_equiv_matrix'_symm_apply

deleted theorem lie_ideal.bot_of_map_eq_bot

deleted theorem lie_ideal.coe_hom_of_le

deleted theorem lie_ideal.coe_to_subalgebra

deleted def lie_ideal.comap

deleted theorem lie_ideal.comap_bracket_eq

deleted theorem lie_ideal.comap_bracket_incl

deleted theorem lie_ideal.comap_bracket_incl_of_le

deleted theorem lie_ideal.comap_bracket_le

deleted theorem lie_ideal.comap_coe_submodule

deleted theorem lie_ideal.comap_incl_self

deleted theorem lie_ideal.comap_map_eq

deleted theorem lie_ideal.comap_map_le

deleted theorem lie_ideal.comap_mono

deleted theorem lie_ideal.derived_series_add_eq_bot

deleted theorem lie_ideal.derived_series_eq_bot_iff

deleted theorem lie_ideal.derived_series_eq_derived_series_of_ideal_comap

deleted theorem lie_ideal.derived_series_eq_derived_series_of_ideal_map

deleted theorem lie_ideal.derived_series_map_le_derived_series

deleted theorem lie_ideal.gc_map_comap

deleted def lie_ideal.hom_of_le

deleted theorem lie_ideal.hom_of_le_apply

deleted theorem lie_ideal.hom_of_le_injective

deleted def lie_ideal.incl

deleted theorem lie_ideal.incl_apply

deleted theorem lie_ideal.incl_coe

deleted theorem lie_ideal.incl_ideal_range

deleted theorem lie_ideal.incl_is_ideal_morphism

deleted theorem lie_ideal.ker_incl

deleted def lie_ideal.map

deleted theorem lie_ideal.map_bracket_le

deleted theorem lie_ideal.map_coe_submodule

deleted theorem lie_ideal.map_comap_bracket_eq

deleted theorem lie_ideal.map_comap_eq

deleted theorem lie_ideal.map_comap_incl

deleted theorem lie_ideal.map_comap_le

deleted theorem lie_ideal.map_le

deleted theorem lie_ideal.map_le_iff_le_comap

deleted theorem lie_ideal.map_mono

deleted theorem lie_ideal.map_of_image

deleted theorem lie_ideal.map_sup_ker_eq_map

deleted theorem lie_ideal.mem_comap

deleted theorem lie_ideal.mem_map

deleted theorem lie_ideal.subsingleton_of_bot

deleted def lie_ideal

deleted def lie_ideal_subalgebra

deleted theorem lie_mem_left

deleted theorem lie_mem_right

deleted theorem lie_module.derived_series_le_lower_central_series

deleted theorem lie_module.is_trivial_iff_maximal_trivial_eq_top

deleted def lie_module.lower_central_series

deleted theorem lie_module.lower_central_series_succ

deleted theorem lie_module.lower_central_series_zero

deleted def lie_module.maximal_trivial_submodule

deleted theorem lie_module.mem_maximal_trivial_submodule

deleted def lie_module.to_endomorphism

deleted theorem lie_module.trivial_iff_le_maximal_trivial

deleted theorem lie_module.trivial_iff_lower_central_eq_bot

deleted theorem lie_ring.of_associative_ring_bracket

deleted theorem lie_subalgebra.add_mem

deleted theorem lie_subalgebra.coe_bracket

deleted theorem lie_subalgebra.coe_injective

deleted theorem lie_subalgebra.coe_set_eq

deleted theorem lie_subalgebra.coe_to_submodule_eq

deleted theorem lie_subalgebra.coe_zero_iff_zero

deleted theorem lie_subalgebra.ext

deleted theorem lie_subalgebra.ext_iff'

deleted theorem lie_subalgebra.ext_iff

deleted def lie_subalgebra.incl

deleted theorem lie_subalgebra.lie_mem

deleted def lie_subalgebra.map

deleted theorem lie_subalgebra.mem_coe'

deleted theorem lie_subalgebra.mem_coe

deleted theorem lie_subalgebra.mem_map_submodule

deleted theorem lie_subalgebra.mk_coe

deleted theorem lie_subalgebra.range_incl

deleted theorem lie_subalgebra.smul_mem

deleted theorem lie_subalgebra.to_submodule_injective

deleted theorem lie_subalgebra.zero_mem

deleted structure lie_subalgebra

deleted def lie_subalgebra_of_subalgebra

deleted theorem lie_submodule.Inf_coe

deleted theorem lie_submodule.Inf_coe_to_submodule

deleted theorem lie_submodule.Inf_glb

deleted theorem lie_submodule.add_eq_sup

deleted theorem lie_submodule.bot_coe

deleted theorem lie_submodule.bot_coe_submodule

deleted theorem lie_submodule.bot_lie

deleted theorem lie_submodule.coe_hom_of_le

deleted theorem lie_submodule.coe_injective

deleted theorem lie_submodule.coe_submodule_injective

deleted theorem lie_submodule.coe_submodule_le_coe_submodule

deleted theorem lie_submodule.coe_to_set_mk

deleted theorem lie_submodule.coe_to_submodule

deleted theorem lie_submodule.coe_to_submodule_eq_iff

deleted theorem lie_submodule.coe_to_submodule_mk

deleted def lie_submodule.comap

deleted theorem lie_submodule.eq_bot_iff

deleted theorem lie_submodule.ext

deleted theorem lie_submodule.gc_map_comap

deleted def lie_submodule.hom_of_le

deleted theorem lie_submodule.hom_of_le_apply

deleted theorem lie_submodule.hom_of_le_injective

deleted def lie_submodule.incl

deleted theorem lie_submodule.incl_apply

deleted theorem lie_submodule.incl_eq_val

deleted theorem lie_submodule.inf_coe

deleted theorem lie_submodule.inf_coe_to_submodule

deleted theorem lie_submodule.inf_lie

deleted theorem lie_submodule.le_def

deleted theorem lie_submodule.lie_abelian_iff_lie_self_eq_bot

deleted theorem lie_submodule.lie_bot

deleted theorem lie_submodule.lie_comm

deleted theorem lie_submodule.lie_ideal_oper_eq_linear_span

deleted theorem lie_submodule.lie_ideal_oper_eq_span

deleted theorem lie_submodule.lie_inf

deleted theorem lie_submodule.lie_le_inf

deleted theorem lie_submodule.lie_le_left

deleted theorem lie_submodule.lie_le_right

deleted theorem lie_submodule.lie_mem_lie

deleted def lie_submodule.lie_span

deleted theorem lie_submodule.lie_span_eq

deleted theorem lie_submodule.lie_span_le

deleted theorem lie_submodule.lie_span_mono

deleted theorem lie_submodule.lie_sup

deleted def lie_submodule.map

deleted theorem lie_submodule.map_le_iff_le_comap

deleted theorem lie_submodule.mem_bot

deleted theorem lie_submodule.mem_carrier

deleted theorem lie_submodule.mem_coe

deleted theorem lie_submodule.mem_coe_submodule

deleted theorem lie_submodule.mem_inf

deleted theorem lie_submodule.mem_lie_span

deleted theorem lie_submodule.mem_sup

deleted theorem lie_submodule.mem_top

deleted theorem lie_submodule.mono_lie

deleted theorem lie_submodule.mono_lie_left

deleted theorem lie_submodule.mono_lie_right

deleted def lie_submodule.quotient.action_as_endo_map

deleted def lie_submodule.quotient.action_as_endo_map_bracket

deleted theorem lie_submodule.quotient.is_quotient_mk

deleted def lie_submodule.quotient.lie_submodule_invariant

deleted def lie_submodule.quotient.mk

deleted theorem lie_submodule.quotient.mk_bracket

deleted def lie_submodule.quotient

deleted theorem lie_submodule.submodule_span_le_lie_span

deleted theorem lie_submodule.subset_lie_span

deleted theorem lie_submodule.subsingleton_of_bot

deleted theorem lie_submodule.sup_coe_to_submodule

deleted theorem lie_submodule.sup_lie

deleted theorem lie_submodule.top_coe

deleted theorem lie_submodule.top_coe_submodule

deleted theorem lie_submodule.trivial_lie_oper_zero

deleted theorem lie_submodule.well_founded_of_noetherian

deleted theorem lie_submodule.zero_mem

deleted structure lie_submodule

deleted def linear_equiv.lie_conj

deleted theorem linear_equiv.lie_conj_apply

deleted theorem linear_equiv.lie_conj_symm

deleted theorem matrix.lie_conj_apply

deleted theorem matrix.lie_conj_symm_apply

deleted def matrix.reindex_lie_equiv

deleted theorem matrix.reindex_lie_equiv_apply

deleted theorem matrix.reindex_lie_equiv_symm_apply

deleted theorem ring_commutator.commutator

deleted theorem trivial_lie_zero

Modified src/algebra/lie/classical.lean

Created src/algebra/lie/ideal_operations.lean

added theorem lie_ideal.comap_bracket_eq

added theorem lie_ideal.comap_bracket_incl

added theorem lie_ideal.comap_bracket_incl_of_le

added theorem lie_ideal.comap_bracket_le

added theorem lie_ideal.map_bracket_le

added theorem lie_ideal.map_comap_bracket_eq

added theorem lie_ideal.map_comap_incl

added theorem lie_submodule.bot_lie

added theorem lie_submodule.inf_lie

added theorem lie_submodule.lie_bot

added theorem lie_submodule.lie_comm

added theorem lie_submodule.lie_ideal_oper_eq_linear_span

added theorem lie_submodule.lie_ideal_oper_eq_span

added theorem lie_submodule.lie_inf

added theorem lie_submodule.lie_le_inf

added theorem lie_submodule.lie_le_left

added theorem lie_submodule.lie_le_right

added theorem lie_submodule.lie_mem_lie

added theorem lie_submodule.lie_sup

added theorem lie_submodule.mono_lie

added theorem lie_submodule.mono_lie_left

added theorem lie_submodule.mono_lie_right

added theorem lie_submodule.sup_lie

Created src/algebra/lie/matrix.lean

added def lie_equiv_matrix'

added theorem lie_equiv_matrix'_apply

added theorem lie_equiv_matrix'_symm_apply

added theorem matrix.lie_conj_apply

added theorem matrix.lie_conj_symm_apply

added def matrix.reindex_lie_equiv

added theorem matrix.reindex_lie_equiv_apply

added theorem matrix.reindex_lie_equiv_symm_apply

Created src/algebra/lie/nilpotent.lean

added theorem lie_module.derived_series_le_lower_central_series

added def lie_module.lower_central_series

added theorem lie_module.lower_central_series_succ

added theorem lie_module.lower_central_series_zero

added theorem lie_module.trivial_iff_lower_central_eq_bot

Created src/algebra/lie/of_associative.lean

added def alg_equiv.to_lie_equiv

added theorem alg_equiv.to_lie_equiv_apply

added theorem alg_equiv.to_lie_equiv_symm_apply

added def lie_algebra.ad

added theorem lie_algebra.ad_apply

added def lie_algebra.of_associative_algebra_hom

added theorem lie_algebra.of_associative_algebra_hom_apply

added theorem lie_algebra.of_associative_algebra_hom_comp

added theorem lie_algebra.of_associative_algebra_hom_id

added def lie_module.to_endomorphism

added theorem lie_ring.of_associative_ring_bracket

added def lie_subalgebra_of_subalgebra

added def linear_equiv.lie_conj

added theorem linear_equiv.lie_conj_apply

added theorem linear_equiv.lie_conj_symm

added theorem ring_commutator.commutator

Created src/algebra/lie/quotient.lean

added def lie_submodule.quotient.action_as_endo_map

added def lie_submodule.quotient.action_as_endo_map_bracket

added theorem lie_submodule.quotient.is_quotient_mk

added def lie_submodule.quotient.lie_submodule_invariant

added def lie_submodule.quotient.mk

added theorem lie_submodule.quotient.mk_bracket

added def lie_submodule.quotient

Created src/algebra/lie/semisimple.lean

added theorem lie_algebra.abelian_radical_iff_solvable_is_abelian

added theorem lie_algebra.abelian_radical_of_semisimple

added theorem lie_algebra.center_eq_bot_of_semisimple

added theorem lie_algebra.is_semisimple_iff_no_abelian_ideals

added theorem lie_algebra.is_semisimple_iff_no_solvable_ideals

added theorem lie_algebra.subsingleton_of_semisimple_lie_abelian

Modified src/algebra/lie/skew_adjoint.lean

Created src/algebra/lie/solvable.lean

added theorem lie_algebra.abelian_derived_abelian_of_ideal

added theorem lie_algebra.abelian_iff_derived_one_eq_bot

added theorem lie_algebra.abelian_iff_derived_succ_eq_bot

added theorem lie_algebra.abelian_of_solvable_ideal_eq_bot_iff

added theorem lie_algebra.center_le_radical

added theorem lie_algebra.derived_length_eq_derived_length_of_ideal

added theorem lie_algebra.derived_length_zero

added def lie_algebra.derived_series

added theorem lie_algebra.derived_series_def

added theorem lie_algebra.derived_series_of_bot_eq_bot

added theorem lie_algebra.derived_series_of_derived_length_succ

added def lie_algebra.derived_series_of_ideal

added theorem lie_algebra.derived_series_of_ideal_add

added theorem lie_algebra.derived_series_of_ideal_add_le_add

added theorem lie_algebra.derived_series_of_ideal_antimono

added theorem lie_algebra.derived_series_of_ideal_le

added theorem lie_algebra.derived_series_of_ideal_le_self

added theorem lie_algebra.derived_series_of_ideal_mono

added theorem lie_algebra.derived_series_of_ideal_succ

added theorem lie_algebra.derived_series_of_ideal_succ_le

added theorem lie_algebra.derived_series_of_ideal_zero

added theorem lie_algebra.is_solvable_of_injective

added theorem lie_algebra.le_solvable_ideal_solvable

added theorem lie_algebra.lie_ideal.solvable_iff_le_radical

added def lie_algebra.radical

added theorem lie_ideal.derived_series_add_eq_bot

added theorem lie_ideal.derived_series_eq_bot_iff

added theorem lie_ideal.derived_series_eq_derived_series_of_ideal_comap

added theorem lie_ideal.derived_series_eq_derived_series_of_ideal_map

added theorem lie_ideal.derived_series_map_le_derived_series

Created src/algebra/lie/subalgebra.lean

added def lie_algebra.equiv.of_eq

added theorem lie_algebra.equiv.of_eq_apply

added theorem lie_algebra.equiv.of_injective_apply

added def lie_algebra.equiv.of_subalgebra

added theorem lie_algebra.equiv.of_subalgebra_apply

added def lie_algebra.equiv.of_subalgebras

added theorem lie_algebra.equiv.of_subalgebras_apply

added theorem lie_algebra.equiv.of_subalgebras_symm_apply

added def lie_algebra.morphism.range

added theorem lie_algebra.morphism.range_bracket

added theorem lie_algebra.morphism.range_coe

added theorem lie_subalgebra.add_mem

added theorem lie_subalgebra.coe_bracket

added theorem lie_subalgebra.coe_injective

added theorem lie_subalgebra.coe_set_eq

added theorem lie_subalgebra.coe_to_submodule_eq

added theorem lie_subalgebra.coe_zero_iff_zero

added theorem lie_subalgebra.ext

added theorem lie_subalgebra.ext_iff'

added theorem lie_subalgebra.ext_iff

added def lie_subalgebra.incl

added theorem lie_subalgebra.lie_mem

added def lie_subalgebra.map

added theorem lie_subalgebra.mem_coe'

added theorem lie_subalgebra.mem_coe

added theorem lie_subalgebra.mem_map_submodule

added theorem lie_subalgebra.mk_coe

added theorem lie_subalgebra.range_incl

added theorem lie_subalgebra.smul_mem

added theorem lie_subalgebra.to_submodule_injective

added theorem lie_subalgebra.zero_mem

added structure lie_subalgebra

Created src/algebra/lie/submodule.lean

added def lie_algebra.morphism.ideal_range

added def lie_algebra.morphism.is_ideal_morphism

added theorem lie_algebra.morphism.is_ideal_morphism_def

added def lie_algebra.morphism.ker

added theorem lie_algebra.morphism.ker_coe_submodule

added theorem lie_algebra.morphism.ker_eq_bot

added theorem lie_algebra.morphism.ker_le_comap

added theorem lie_algebra.morphism.le_ker_iff

added theorem lie_algebra.morphism.map_bot_iff

added theorem lie_algebra.morphism.map_le_ideal_range

added theorem lie_algebra.morphism.mem_ideal_range

added theorem lie_algebra.morphism.mem_ideal_range_iff

added theorem lie_algebra.morphism.mem_ker

added theorem lie_algebra.morphism.range_subset_ideal_range

added def lie_algebra.top_equiv_self

added theorem lie_algebra.top_equiv_self_apply

added theorem lie_ideal.bot_of_map_eq_bot

added theorem lie_ideal.coe_hom_of_le

added theorem lie_ideal.coe_to_subalgebra

added def lie_ideal.comap

added theorem lie_ideal.comap_coe_submodule

added theorem lie_ideal.comap_incl_self

added theorem lie_ideal.comap_map_eq

added theorem lie_ideal.comap_map_le

added theorem lie_ideal.comap_mono

added theorem lie_ideal.gc_map_comap

added def lie_ideal.hom_of_le

added theorem lie_ideal.hom_of_le_apply

added theorem lie_ideal.hom_of_le_injective

added def lie_ideal.incl

added theorem lie_ideal.incl_apply

added theorem lie_ideal.incl_coe

added theorem lie_ideal.incl_ideal_range

added theorem lie_ideal.incl_is_ideal_morphism

added theorem lie_ideal.ker_incl

added def lie_ideal.map

added theorem lie_ideal.map_coe_submodule

added theorem lie_ideal.map_comap_eq

added theorem lie_ideal.map_comap_le

added theorem lie_ideal.map_le

added theorem lie_ideal.map_le_iff_le_comap

added theorem lie_ideal.map_mono

added theorem lie_ideal.map_of_image

added theorem lie_ideal.map_sup_ker_eq_map

added theorem lie_ideal.mem_comap

added theorem lie_ideal.mem_map

added theorem lie_ideal.subsingleton_of_bot

added def lie_ideal

added def lie_ideal_subalgebra

added theorem lie_mem_left

added theorem lie_mem_right

added theorem lie_submodule.Inf_coe

added theorem lie_submodule.Inf_coe_to_submodule

added theorem lie_submodule.Inf_glb

added theorem lie_submodule.add_eq_sup

added theorem lie_submodule.bot_coe

added theorem lie_submodule.bot_coe_submodule

added theorem lie_submodule.coe_hom_of_le

added theorem lie_submodule.coe_injective

added theorem lie_submodule.coe_submodule_injective

added theorem lie_submodule.coe_submodule_le_coe_submodule

added theorem lie_submodule.coe_to_set_mk

added theorem lie_submodule.coe_to_submodule

added theorem lie_submodule.coe_to_submodule_eq_iff

added theorem lie_submodule.coe_to_submodule_mk

added def lie_submodule.comap

added theorem lie_submodule.eq_bot_iff

added theorem lie_submodule.ext

added theorem lie_submodule.gc_map_comap

added def lie_submodule.hom_of_le

added theorem lie_submodule.hom_of_le_apply

added theorem lie_submodule.hom_of_le_injective

added def lie_submodule.incl

added theorem lie_submodule.incl_apply

added theorem lie_submodule.incl_eq_val

added theorem lie_submodule.inf_coe

added theorem lie_submodule.inf_coe_to_submodule

added theorem lie_submodule.le_def

added def lie_submodule.lie_span

added theorem lie_submodule.lie_span_eq

added theorem lie_submodule.lie_span_le

added theorem lie_submodule.lie_span_mono

added def lie_submodule.map

added theorem lie_submodule.map_le_iff_le_comap

added theorem lie_submodule.mem_bot

added theorem lie_submodule.mem_carrier

added theorem lie_submodule.mem_coe

added theorem lie_submodule.mem_coe_submodule

added theorem lie_submodule.mem_inf

added theorem lie_submodule.mem_lie_span

added theorem lie_submodule.mem_sup

added theorem lie_submodule.mem_top

added theorem lie_submodule.submodule_span_le_lie_span

added theorem lie_submodule.subset_lie_span

added theorem lie_submodule.subsingleton_of_bot

added theorem lie_submodule.sup_coe_to_submodule

added theorem lie_submodule.top_coe

added theorem lie_submodule.top_coe_submodule

added theorem lie_submodule.well_founded_of_noetherian

added theorem lie_submodule.zero_mem

added structure lie_submodule

Modified src/algebra/lie/universal_enveloping.lean

Modified src/ring_theory/derivation.lean