Commit 2024-05-07 18:06 e0219f6c

View on Github →

chore: split Mathlib.Algebra.Lie.Killing (#12735)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Lie/Killing.lean

deleted theorem LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace

deleted theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton

deleted theorem LieAlgebra.IsKilling.corootSpace_eq_bot_iff

deleted theorem LieAlgebra.IsKilling.corootSpace_zero_eq_bot

deleted theorem LieAlgebra.IsKilling.coroot_eq_zero_iff

deleted theorem LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace

deleted theorem LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace

deleted theorem LieAlgebra.IsKilling.iInf_ker_weight_eq_bot

deleted theorem LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot

deleted theorem LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra

deleted theorem LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra

deleted theorem LieAlgebra.IsKilling.restrict_killingForm

deleted theorem LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero

deleted theorem LieAlgebra.IsKilling.root_apply_coroot

deleted theorem LieAlgebra.IsKilling.span_weight_eq_top

deleted theorem LieAlgebra.IsKilling.traceForm_cartan_nondegenerate

deleted theorem LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero

deleted theorem LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg

deleted theorem LieIdeal.coe_killingCompl_top

deleted theorem LieIdeal.killingForm_eq

deleted theorem LieIdeal.le_killingCompl_top_of_isLieAbelian

deleted theorem LieIdeal.mem_killingCompl

deleted theorem LieIdeal.restrict_killingForm

deleted theorem LieIdeal.toSubmodule_killingCompl

deleted theorem LieModule.eq_zero_of_mem_weightSpace_mem_posFitting

deleted theorem LieModule.isLieAbelian_of_ker_traceForm_eq_bot

deleted theorem LieModule.lie_traceForm_eq_zero

deleted theorem LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm

deleted theorem LieModule.range_traceForm_le_span_weight

deleted theorem LieModule.traceForm_apply_apply

deleted theorem LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center

deleted theorem LieModule.traceForm_apply_lie_apply'

deleted theorem LieModule.traceForm_apply_lie_apply

deleted theorem LieModule.traceForm_comm

deleted theorem LieModule.traceForm_eq_sum_finrank_nsmul

deleted theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul

deleted theorem LieModule.traceForm_eq_sum_weightSpaceOf

deleted theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs

deleted theorem LieModule.traceForm_eq_zero_of_isNilpotent

deleted theorem LieModule.traceForm_eq_zero_of_isTrivial

deleted theorem LieModule.traceForm_flip

deleted theorem LieModule.traceForm_isSymm

deleted theorem LieModule.traceForm_lieSubalgebra_mk_left

deleted theorem LieModule.traceForm_lieSubalgebra_mk_right

deleted theorem LieModule.traceForm_weightSpace_eq

deleted theorem LieModule.trace_toEndomorphism_eq_zero_of_mem_lcs

deleted theorem LieSubmodule.traceForm_eq_of_le_idealizer

deleted theorem LieSubmodule.traceForm_eq_zero_of_isTrivial

deleted theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer

deleted theorem killingForm_apply_apply

deleted theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting

Created Mathlib/Algebra/Lie/TraceForm.lean

added theorem LieIdeal.coe_killingCompl_top

added theorem LieIdeal.killingForm_eq

added theorem LieIdeal.le_killingCompl_top_of_isLieAbelian

added theorem LieIdeal.mem_killingCompl

added theorem LieIdeal.restrict_killingForm

added theorem LieIdeal.toSubmodule_killingCompl

added theorem LieModule.eq_zero_of_mem_weightSpace_mem_posFitting

added theorem LieModule.isLieAbelian_of_ker_traceForm_eq_bot

added theorem LieModule.lie_traceForm_eq_zero

added theorem LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm

added theorem LieModule.range_traceForm_le_span_weight

added theorem LieModule.traceForm_apply_apply

added theorem LieModule.traceForm_apply_eq_zero_of_mem_lcs_of_mem_center

added theorem LieModule.traceForm_apply_lie_apply'

added theorem LieModule.traceForm_apply_lie_apply

added theorem LieModule.traceForm_comm

added theorem LieModule.traceForm_eq_sum_finrank_nsmul

added theorem LieModule.traceForm_eq_sum_finrank_nsmul_mul

added theorem LieModule.traceForm_eq_sum_weightSpaceOf

added theorem LieModule.traceForm_eq_zero_if_mem_lcs_of_mem_ucs

added theorem LieModule.traceForm_eq_zero_of_isNilpotent

added theorem LieModule.traceForm_eq_zero_of_isTrivial

added theorem LieModule.traceForm_flip

added theorem LieModule.traceForm_isSymm

added theorem LieModule.traceForm_lieSubalgebra_mk_left

added theorem LieModule.traceForm_lieSubalgebra_mk_right

added theorem LieModule.traceForm_weightSpace_eq

added theorem LieModule.trace_toEndomorphism_eq_zero_of_mem_lcs

added theorem LieSubmodule.traceForm_eq_of_le_idealizer

added theorem LieSubmodule.traceForm_eq_zero_of_isTrivial

added theorem LieSubmodule.trace_eq_trace_restrict_of_le_idealizer

added theorem killingForm_apply_apply

added theorem killingForm_eq_zero_of_mem_zeroRoot_mem_posFitting

Created Mathlib/Algebra/Lie/Weights/Killing.lean

added theorem LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace

added theorem LieAlgebra.IsKilling.coe_corootSpace_eq_span_singleton

added theorem LieAlgebra.IsKilling.corootSpace_eq_bot_iff

added theorem LieAlgebra.IsKilling.corootSpace_zero_eq_bot

added theorem LieAlgebra.IsKilling.coroot_eq_zero_iff

added theorem LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace

added theorem LieAlgebra.IsKilling.eq_zero_of_apply_eq_zero_of_mem_corootSpace

added theorem LieAlgebra.IsKilling.iInf_ker_weight_eq_bot

added theorem LieAlgebra.IsKilling.isCompl_ker_weight_span_coroot

added theorem LieAlgebra.IsKilling.ker_restrict_eq_bot_of_isCartanSubalgebra

added theorem LieAlgebra.IsKilling.ker_traceForm_eq_bot_of_isCartanSubalgebra

added theorem LieAlgebra.IsKilling.restrict_killingForm

added theorem LieAlgebra.IsKilling.root_apply_cartanEquivDual_symm_ne_zero

added theorem LieAlgebra.IsKilling.root_apply_coroot

added theorem LieAlgebra.IsKilling.span_weight_eq_top

added theorem LieAlgebra.IsKilling.traceForm_cartan_nondegenerate

added theorem LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero

added theorem LieAlgebra.mem_ker_killingForm_of_mem_rootSpace_of_forall_rootSpace_neg