Mathlib Changelog
v3
Changelog
About
Github
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