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

deleted def is_lie_abelian
deleted def lie_algebra.ad
deleted theorem lie_algebra.ad_apply
deleted def lie_algebra.center
deleted def lie_algebra.radical
deleted def lie_equiv_matrix'
deleted theorem lie_equiv_matrix'_apply
deleted theorem lie_ideal.coe_hom_of_le
deleted def lie_ideal.comap
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.gc_map_comap
deleted def lie_ideal.hom_of_le
deleted theorem lie_ideal.hom_of_le_apply
deleted def lie_ideal.incl
deleted theorem lie_ideal.incl_apply
deleted theorem lie_ideal.incl_coe
deleted theorem lie_ideal.ker_incl
deleted def lie_ideal.map
deleted theorem lie_ideal.map_bracket_le
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_mono
deleted theorem lie_ideal.map_of_image
deleted theorem lie_ideal.mem_comap
deleted theorem lie_ideal.mem_map
deleted def lie_ideal
deleted theorem lie_mem_left
deleted theorem lie_mem_right
deleted theorem lie_subalgebra.add_mem
deleted theorem lie_subalgebra.coe_set_eq
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.mk_coe
deleted theorem lie_subalgebra.range_incl
deleted theorem lie_subalgebra.smul_mem
deleted theorem lie_subalgebra.zero_mem
deleted structure lie_subalgebra
deleted theorem lie_submodule.Inf_coe
deleted theorem lie_submodule.Inf_glb
deleted theorem lie_submodule.add_eq_sup
deleted theorem lie_submodule.bot_coe
deleted theorem lie_submodule.bot_lie
deleted def lie_submodule.comap
deleted theorem lie_submodule.eq_bot_iff
deleted theorem lie_submodule.ext
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_lie
deleted theorem lie_submodule.le_def
deleted theorem lie_submodule.lie_bot
deleted theorem lie_submodule.lie_comm
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_mem_lie
deleted theorem lie_submodule.lie_span_eq
deleted theorem lie_submodule.lie_span_le
deleted theorem lie_submodule.lie_sup
deleted def lie_submodule.map
deleted theorem lie_submodule.mem_bot
deleted theorem lie_submodule.mem_carrier
deleted theorem lie_submodule.mem_coe
deleted theorem lie_submodule.mem_inf
deleted theorem lie_submodule.mem_sup
deleted theorem lie_submodule.mem_top
deleted theorem lie_submodule.mono_lie
deleted theorem lie_submodule.sup_lie
deleted theorem lie_submodule.top_coe
deleted theorem lie_submodule.zero_mem
deleted structure lie_submodule
deleted theorem matrix.lie_conj_apply
deleted theorem trivial_lie_zero
added def lie_ideal.comap
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.incl
added theorem lie_ideal.incl_apply
added theorem lie_ideal.incl_coe
added theorem lie_ideal.ker_incl
added def lie_ideal.map
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_mono
added theorem lie_ideal.map_of_image
added theorem lie_ideal.mem_comap
added theorem lie_ideal.mem_map
added def lie_ideal
added theorem lie_mem_left
added theorem lie_mem_right
added theorem lie_submodule.Inf_coe
added theorem lie_submodule.Inf_glb
added theorem lie_submodule.bot_coe
added theorem lie_submodule.ext
added theorem lie_submodule.inf_coe
added theorem lie_submodule.le_def
added theorem lie_submodule.mem_bot
added theorem lie_submodule.mem_coe
added theorem lie_submodule.mem_inf
added theorem lie_submodule.mem_sup
added theorem lie_submodule.mem_top
added theorem lie_submodule.top_coe
added theorem lie_submodule.zero_mem
added structure lie_submodule