Abelian

📁 Source: Mathlib/Algebra/Lie/Abelian.lean

Statistics

Metric	Count
Definitions IsLieAbelian, center, IsTrivial, ker, maxTrivEquiv, maxTrivHom, maxTrivLinearMapEquivLieModuleHom, maxTrivSubmodule, TrivialLieModule, equiv, instAddCommGroup, instLieRingModule, instModule	13
Theorems isLieAbelian, isLieAbelian, abelian_of_le_center, ad_ker_eq_self_module_ker, center_eq_bot, instIsLieAbelianSubtypeMemLieSubmoduleCenter, isFaithful_self_iff, isLieAbelian_iff_center_eq_top, self_module_ker_eq_center, isLieAbelian_iff, isLieAbelian_of_trivial, trivial, coe_maxTrivEquiv_apply, coe_maxTrivHom_apply, coe_maxTrivLinearMapEquivLieModuleHom, coe_maxTrivLinearMapEquivLieModuleHom_symm, commute_toEnd_of_mem_center_left, commute_toEnd_of_mem_center_right, ideal_oper_maxTrivSubmodule_eq_bot, instIsTrivialOfSubsingleton, instIsTrivialOfSubsingleton', instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, isFaithful_iff_ker_eq_bot, isTrivial_iff_max_triv_eq_top, ker_eq_bot, le_max_triv_iff_bracket_eq_bot, maxTrivEquiv_of_equiv_symm_eq_symm, maxTrivEquiv_of_refl_eq_refl, mem_ker, mem_maxTrivSubmodule, toLinearMap_maxTrivLinearMapEquivLieModuleHom, toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, trivial_iff_le_maximal_trivial, isLieAbelian_lieSpan_iff, lie_abelian_iff_lie_self_eq_bot, trivial_lie_oper_zero, instIsTrivial, instLieModule, commutative_ring_iff_abelian_lie_ring, lie_abelian_iff_equiv_lie_abelian, lie_eq_self_of_isAtom_of_ne_bot, lie_eq_self_of_isAtom_of_nonabelian, trivial_lie_zero	43
Total	56

Function.Injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLieAbelian 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike	IsLieAbelian LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LieHom.map_lie trivial_lie_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLieAbelian 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike	IsLieAbelian LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	LieHom.map_lie trivial_lie_zero map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass

LieAlgebra

Definitions

Name	Category	Theorems
center 📖	CompOp	13 math math: hasCentralRadical_iff, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, non_trivial_center_of_isNilpotent, hasCentralRadical_and_of_isIrreducible_of_isFaithful, self_module_ker_eq_center, HasCentralRadical.radical_eq_center, center_le_radical, center_eq_bot, isLieAbelian_iff_center_eq_top, isFaithful_self_iff, instIsLieAbelianSubtypeMemLieSubmoduleCenter, center_le_maxNilpotentIdeal, LieDerivation.ad_ker_eq_center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abelian_of_le_center 📖	mathematical	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup toModule lieRingSelfModule center	IsLieAbelian LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass	—	LieIdeal.isLieAbelian_of_trivial LieSubmodule.instAddSubgroupClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass lieAlgebraSelfModule LieModule.trivial_iff_le_maximal_trivial
ad_ker_eq_self_module_ker 📖	mathematical	—	LieHom.ker Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup toModule LieRing.ofAssociativeRing Module.End.instRing ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero ad LieModule.ker lieRingSelfModule lieAlgebraSelfModule	—	smulCommClass_self IsScalarTower.left
center_eq_bot 📖	mathematical	—	center Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup toModule lieRingSelfModule	—	lieAlgebraSelfModule isFaithful_self_iff
instIsLieAbelianSubtypeMemLieSubmoduleCenter 📖	mathematical	—	IsLieAbelian LieSubmodule LieRing.toAddCommGroup toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike center LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass LieIdeal.isLieAbelian_of_trivial LieModule.instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule lieAlgebraSelfModule
isFaithful_self_iff 📖	mathematical	—	LieModule.IsFaithful LieRing.toAddCommGroup toModule lieRingSelfModule lieAlgebraSelfModule center Bot.bot LieIdeal LieSubmodule.instBot	—	lieAlgebraSelfModule LieModule.isFaithful_iff_ker_eq_bot self_module_ker_eq_center
isLieAbelian_iff_center_eq_top 📖	mathematical	—	IsLieAbelian LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid center Top.top LieIdeal LieSubmodule.instTop toModule	—	LieModule.isTrivial_iff_max_triv_eq_top lieAlgebraSelfModule
self_module_ker_eq_center 📖	mathematical	—	LieModule.ker LieRing.toAddCommGroup toModule lieRingSelfModule lieAlgebraSelfModule center	—	LieSubmodule.ext lieAlgebraSelfModule lie_skew

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLieAbelian_iff 📖	mathematical	—	IsLieAbelian LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket lieRing lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieModule.ker lieAlgebra LieSubmodule.instLieModule lieAlgebraSelfModule	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass LieSubmodule.instLieModule lieAlgebraSelfModule LieHom.mem_ker LinearMap.ext LieModule.IsTrivial.trivial coe_bracket_of_module LinearMap.congr_fun
isLieAbelian_of_trivial 📖	mathematical	—	IsLieAbelian LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket lieRing lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass	—	LieSubmodule.instAddSubgroupClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieModule.IsTrivial.trivial

LieModule

Definitions

Name	Category	Theorems
IsTrivial 📖	CompData	10 math math: trivial_iff_lower_central_eq_bot, instIsTrivialOfSubsingleton', trivial_iff_le_maximal_trivial, instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, disjoint_lowerCentralSeries_maxTrivSubmodule_iff, isTrivial_of_nilpotencyLength_le_one, nilpotencyLength_eq_one_iff, instIsTrivialOfSubsingleton, isTrivial_iff_max_triv_eq_top, TrivialLieModule.instIsTrivial
ker 📖	CompOp	6 math math: mem_ker, LieAlgebra.self_module_ker_eq_center, LieIdeal.isLieAbelian_iff, isFaithful_iff_ker_eq_bot, LieAlgebra.ad_ker_eq_self_module_ker, ker_eq_bot
maxTrivEquiv 📖	CompOp	3 math math: maxTrivEquiv_of_equiv_symm_eq_symm, maxTrivEquiv_of_refl_eq_refl, coe_maxTrivEquiv_apply
maxTrivHom 📖	CompOp	1 math math: coe_maxTrivHom_apply
maxTrivLinearMapEquivLieModuleHom 📖	CompOp	4 math math: toLinearMap_maxTrivLinearMapEquivLieModuleHom, toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, coe_maxTrivLinearMapEquivLieModuleHom_symm, coe_maxTrivLinearMapEquivLieModuleHom
maxTrivSubmodule 📖	CompOp	22 math math: trivial_iff_le_maximal_trivial, instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule, toLinearMap_maxTrivLinearMapEquivLieModuleHom, disjoint_lowerCentralSeries_maxTrivSubmodule_iff, nontrivial_max_triv_of_isNilpotent, LinearMap.BilinForm.lieInvariant_iff, mem_maxTrivSubmodule, toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm, lowerCentralSeriesLast_le_max_triv, ideal_oper_maxTrivSubmodule_eq_bot, maxTrivEquiv_of_equiv_symm_eq_symm, le_max_triv_iff_bracket_eq_bot, maxTrivEquiv_of_refl_eq_refl, LieSubalgebra.normalizer_eq_self_iff, isTrivial_iff_max_triv_eq_top, coe_maxTrivLinearMapEquivLieModuleHom_symm, coe_maxTrivEquiv_apply, coe_maxTrivHom_apply, LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot, LieSubmodule.ucs_bot_one, coe_maxTrivLinearMapEquivLieModuleHom, LieSubmodule.normalizer_bot_eq_maxTrivSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_maxTrivEquiv_apply 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule DFunLike.coe LieModuleEquiv AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem EquivLike.toFunLike LieModuleEquiv.instEquivLike maxTrivEquiv	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
coe_maxTrivHom_apply 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule DFunLike.coe LieModuleHom AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem LieModuleHom.instFunLike maxTrivHom	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
coe_maxTrivLinearMapEquivLieModuleHom 📖	mathematical	—	DFunLike.coe LieModuleHom LieModuleHom.instFunLike LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid LieSubmodule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule LinearMap.instLieModule AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieModuleHom.instAddCommGroup SubmoduleClass.module LinearMap.addCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieModuleHom.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv maxTrivLinearMapEquivLieModuleHom LinearMap.instFunLike	—	smulCommClass_self LinearMap.instLieModule RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
coe_maxTrivLinearMapEquivLieModuleHom_symm 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike LieSubmodule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule LinearMap.instLieModule LinearEquiv RingHomInvPair.ids LieModuleHom LieModuleHom.instAddCommGroup AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieModuleHom.instModule SubmoduleClass.module LinearMap.addCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm maxTrivLinearMapEquivLieModuleHom LieModuleHom.instFunLike	—	smulCommClass_self LinearMap.instLieModule RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
commute_toEnd_of_mem_center_left 📖	mathematical	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieAlgebra.center	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.End.instMul DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd	—	smulCommClass_self IsScalarTower.left Commute.symm_iff commute_iff_lie_eq LieHom.map_lie map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LieHom.instLinearMapClass
commute_toEnd_of_mem_center_right 📖	mathematical	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieAlgebra.center	Commute Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.End.instMul DFunLike.coe LieHom LieRing.ofAssociativeRing Module.End.instRing LieAlgebra.ofAssociativeAlgebra Module.End.instAlgebra smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero LieHom.instFunLike toEnd	—	Commute.symm smulCommClass_self IsScalarTower.left commute_toEnd_of_mem_center_left
ideal_oper_maxTrivSubmodule_eq_bot 📖	mathematical	—	Bracket.bracket LieIdeal LieSubmodule LieSubmodule.hasBracket maxTrivSubmodule Bot.bot LieSubmodule.instBot	—	LieSubmodule.lieIdeal_oper_eq_linear_span LieSubmodule.bot_toSubmodule Submodule.span_eq_bot
instIsTrivialOfSubsingleton 📖	mathematical	—	IsTrivial LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Subsingleton.eq_zero zero_lie
instIsTrivialOfSubsingleton' 📖	mathematical	—	IsTrivial LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Subsingleton.eq_zero lie_zero
instIsTrivialSubtypeMemLieSubmoduleMaxTrivSubmodule 📖	mathematical	—	IsTrivial LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule LieRingModule.toBracket AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass	—	LieSubmodule.instAddSubgroupClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass
isFaithful_iff_ker_eq_bot 📖	mathematical	—	IsFaithful ker Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	isFaithful_iff' LieSubmodule.ext_iff zero_lie
isTrivial_iff_max_triv_eq_top 📖	mathematical	—	IsTrivial LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid maxTrivSubmodule Top.top LieSubmodule LieSubmodule.instTop	—	LieSubmodule.ext Zero.instNonempty mem_maxTrivSubmodule LieSubmodule.mem_top
ker_eq_bot 📖	mathematical	—	ker Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	isFaithful_iff_ker_eq_bot
le_max_triv_iff_bracket_eq_bot 📖	mathematical	—	LieSubmodule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder maxTrivSubmodule Bracket.bracket LieIdeal LieSubmodule.hasBracket Top.top LieSubmodule.instTop LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule Bot.bot LieSubmodule.instBot	—	le_bot_iff ideal_oper_maxTrivSubmodule_eq_bot LieSubmodule.mono_lie_right mem_maxTrivSubmodule LieSubmodule.lie_eq_bot_iff LieSubmodule.mem_top
maxTrivEquiv_of_equiv_symm_eq_symm 📖	mathematical	—	LieModuleEquiv.symm LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem maxTrivEquiv	—	LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
maxTrivEquiv_of_refl_eq_refl 📖	mathematical	—	maxTrivEquiv LieModuleEquiv.refl LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass SubmoduleClass.module CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieSubmodule.instLieRingModuleSubtypeMem	—	LieModuleEquiv.ext LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
mem_ker 📖	mathematical	—	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule ker Bracket.bracket LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mem_maxTrivSubmodule 📖	mathematical	—	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule Bracket.bracket LieRingModule.toBracket NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
toLinearMap_maxTrivLinearMapEquivLieModuleHom 📖	mathematical	—	LieModuleHom.toLinearMap DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap AddCommGroup.toAddCommMonoid LieSubmodule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule LinearMap.instLieModule LieModuleHom AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieModuleHom.instAddCommGroup SubmoduleClass.module LinearMap.addCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass LieModuleHom.instModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv maxTrivLinearMapEquivLieModuleHom	—	smulCommClass_self LinearMap.instLieModule LinearMap.ext RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
toLinearMap_maxTrivLinearMapEquivLieModuleHom_symm 📖	mathematical	—	LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LieSubmodule LinearMap.addCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Ring.toSemiring CommRing.toRing LinearMap.instLieRingModule SetLike.instMembership LieSubmodule.instSetLike maxTrivSubmodule LinearMap.instLieModule DFunLike.coe LinearEquiv RingHomInvPair.ids LieModuleHom LieModuleHom.instAddCommGroup AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieModuleHom.instModule SubmoduleClass.module LinearMap.addCommMonoid AddCommGroup.toAddGroup LieSubmodule.instSMulMemClass EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm maxTrivLinearMapEquivLieModuleHom LieModuleHom.toLinearMap	—	smulCommClass_self LinearMap.instLieModule RingHomInvPair.ids LieSubmodule.instAddSubgroupClass LieSubmodule.instSMulMemClass
trivial_iff_le_maximal_trivial 📖	mathematical	—	IsTrivial LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder maxTrivSubmodule	—	LieSubmodule.instAddSubgroupClass AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass

LieModule.IsTrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
trivial 📖	mathematical	—	Bracket.bracket	—	—

LieSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLieAbelian_lieSpan_iff 📖	mathematical	—	IsLieAbelian LieSubalgebra SetLike.instMembership instSetLike lieSpan LieRingModule.toBracket lieRing LieRing.toAddCommGroup lieRingSelfModule ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass Bracket.bracket	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass subset_lieSpan trivial_lie_zero lieSpan_induction zero_mem lie_zero add_mem lie_add add_zero smul_mem lie_smul lieAlgebraSelfModule smul_zero lie_mem leibniz_lie instIsLieTower zero_lie add_lie smul_lie lie_lie sub_self

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lie_abelian_iff_lie_self_eq_bot 📖	mathematical	—	IsLieAbelian LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership instSetLike LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass Bracket.bracket LieIdeal hasBracket Bot.bot instBot	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass instAddSubgroupClass LieSubalgebra.coe_bracket LieSubalgebra.instAddSubgroupClass LieSubalgebra.coe_zero_iff_zero LieModule.IsTrivial.trivial
trivial_lie_oper_zero 📖	mathematical	—	Bracket.bracket LieIdeal LieSubmodule hasBracket Bot.bot instBot	—	lieIdeal_oper_eq_span lieSpan_le trivial_lie_zero le_bot_iff

TrivialLieModule

Definitions

Name	Category	Theorems
equiv 📖	CompOp	1 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply
instAddCommGroup 📖	CompOp	4 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, instLieModule, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, instIsTrivial
instLieRingModule 📖	CompOp	3 math math: instLieModule, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, instIsTrivial
instModule 📖	CompOp	3 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, instLieModule, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsTrivial 📖	mathematical	—	LieModule.IsTrivial TrivialLieModule LieRingModule.toBracket instAddCommGroup instLieRingModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
instLieModule 📖	mathematical	—	LieModule TrivialLieModule instAddCommGroup instModule instLieRingModule	—	trivial_lie_zero instIsTrivial smul_zero

(root)

Definitions

Name	Category	Theorems
IsLieAbelian 📖	MathDef	25 math math: Function.Surjective.isLieAbelian, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieSubalgebra.isLieAbelian_lieSpan_iff, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraCartanSubalgebra, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieAlgebra.derivedSeries_of_derivedLength_succ, LieAlgebra.abelian_radical_iff_solvable_is_abelian, commutative_ring_iff_abelian_lie_ring, lie_abelian_iff_equiv_lie_abelian, Function.Injective.isLieAbelian, LieIdeal.isLieAbelian_iff, LieAlgebra.abelian_iff_derived_one_eq_bot, RootPairing.GeckConstruction.instIsLieAbelianSubtypeMatrixSumMemFinsetSupportLieSubalgebraLieAlgebraCartanSubalgebra', LieAlgebra.isLieAbelian_iff_center_eq_top, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, LieModule.isLieAbelian_of_ker_traceForm_eq_bot, LieIdeal.isLieAbelian_of_trivial, LieAlgebra.abelian_derivedAbelianOfIdeal, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieAlgebra.IsSimple.non_abelian, LieAlgebra.SpecialLinear.sl_non_abelian, LieAlgebra.IsKilling.instIsLieAbelianOfIsCartanSubalgebra
TrivialLieModule 📖	CompOp	4 math math: LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply, TrivialLieModule.instLieModule, LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe, TrivialLieModule.instIsTrivial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutative_ring_iff_abelian_lie_ring 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing IsLieAbelian LieRingModule.toBracket LieRing.ofAssociativeRing LieRing.toAddCommGroup lieRingSelfModule MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	LieModule.IsTrivial.trivial
lie_abelian_iff_equiv_lie_abelian 📖	mathematical	—	IsLieAbelian LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	Function.Injective.isLieAbelian LieEquiv.injective
lie_eq_self_of_isAtom_of_ne_bot 📖	mathematical	IsAtom LieSubmodule PartialOrder.toPreorder LieSubmodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice	Bracket.bracket LieIdeal LieSubmodule.hasBracket	—	IsAtom.le_iff_eq LieSubmodule.lie_le_right
lie_eq_self_of_isAtom_of_nonabelian 📖	mathematical	IsAtom LieIdeal PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule BoundedOrder.toOrderBot Preorder.toLE CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice IsLieAbelian LieSubmodule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule LieSubmodule.instLieRingModuleSubtypeMem ZeroMemClass.zero NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddSubmonoidClass.toZeroMemClass AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass	Bracket.bracket LieSubmodule.hasBracket	—	AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass lie_eq_self_of_isAtom_of_ne_bot not_imp_not LieSubmodule.lie_abelian_iff_lie_self_eq_bot
trivial_lie_zero 📖	mathematical	—	Bracket.bracket	—	LieModule.IsTrivial.trivial

---

← Back to Index