Ideal

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

Statistics

Metric	Count
Definitions IsIdealMorphism, idealRange, ker, LieIdeal, comap, incl, inclusion, lieAlgebra, lieRing, lieRingModule, map, toLieSubalgebra, topEquiv, instCoeLieIdealLieSubalgebra	14
Theorems eq, idealRange_eq_lieSpan_range, idealRange_eq_map, idealRange_eq_top_of_surjective, isIdealMorphism_def, isIdealMorphism_iff, isIdealMorphism_of_surjective, ker_eq_bot, ker_le_comap, ker_toSubmodule, le_ker_iff, map_le_idealRange, mem_idealRange, mem_idealRange_iff, mem_ker, range_eq_top, range_subset_idealRange, range_toSubmodule, bot_of_map_eq_bot, coe_bracket_of_module, coe_inclusion, coe_map_of_surjective, coe_toLieSubalgebra, comap_incl_eq_bot, comap_incl_eq_top, comap_incl_self, comap_map_eq, comap_map_le, comap_mono, comap_toSubmodule, gc_map_comap, incl_apply, incl_coe, incl_idealRange, incl_injective, incl_isIdealMorphism, incl_range, inclusion_apply, inclusion_injective, ker_incl, lieModule, map_comap_eq, map_comap_le, map_eq_bot_iff, map_le, map_le_iff_le_comap, map_mono, map_of_image, map_sup, map_sup_ker_eq_map, map_sup_ker_eq_map', map_toSubmodule, mem_comap, mem_map, mem_map_of_surjective, subsingleton_of_bot, toLieSubalgebra_toSubmodule, topEquiv_apply, top_toLieSubalgebra, exists_lieIdeal_coe_eq_iff, exists_nested_lieIdeal_coe_eq_iff, instIsLieTowerSubtypeMemLieSubmodule, instIsLieTowerSubtypeMemLieSubmodule_1, lie_mem_left, lie_mem_right	65
Total	79

LieHom

Definitions

Name	Category	Theorems
IsIdealMorphism 📖	MathDef	5 math math: isIdealMorphism_of_surjective, isIdealMorphism_def, LieIdeal.incl_isIdealMorphism, LieDerivation.ad_isIdealMorphism, isIdealMorphism_iff
idealRange 📖	CompOp	14 math math: isIdealMorphism_def, mem_idealRange, IsIdealMorphism.eq, LieIdeal.map_comap_bracket_eq, idealRange_eq_map, idealRange_eq_lieSpan_range, LieIdeal.incl_idealRange, LieIdeal.map_comap_eq, range_subset_idealRange, map_le_idealRange, mem_idealRange_iff, LieDerivation.mem_ad_idealRange_iff, LieIdeal.comap_bracket_eq, idealRange_eq_top_of_surjective
ker 📖	CompOp	30 math math: LieAlgebra.Extension.incl_apply_mem_ker, quotKerEquivRange_toFun, LieAlgebra.Extension.toKer_bracket, LieAlgebra.Extension.lie_incl_mem_ker, ker_eq_bot, LieAlgebra.Extension.ringModuleOf_bracket, ker_le_comap, LieIdeal.map_sup_ker_eq_map', LieAlgebra.IsExtension.ker_eq_bot, quotKerEquivRange_invFun, LieIdeal.comap_map_eq, mem_ker, LieAlgebra.IsExtension.exact, LieAlgebra.Extension.lie_apply_proj_of_leftInverse_eq, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, ker_toSubmodule, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieDerivation.ad_ker_eq_center, le_ker_iff, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieIdeal.comap_bracket_eq, LieAlgebra.ad_ker_eq_self_module_ker, LieIdeal.map_sup_ker_eq_map, LieAlgebra.Extension.lie_toKer_apply, range_eq_ker_iff, LieIdeal.ker_incl, LieIdeal.map_eq_bot_iff, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieAlgebra.isExtension_of_surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealRange_eq_lieSpan_range 📖	mathematical	—	idealRange LieSubmodule.lieSpan LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.coe LieSubalgebra LieSubalgebra.instSetLike range	—	—
idealRange_eq_map 📖	mathematical	—	idealRange LieIdeal.map Top.top LieIdeal LieSubmodule.instTop LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	LieSubmodule.ext range_eq_map
idealRange_eq_top_of_surjective 📖	mathematical	DFunLike.coe LieHom instFunLike	idealRange Top.top LieIdeal LieSubmodule.instTop LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	idealRange_eq_lieSpan_range range_eq_top LieSubalgebra.coe_toSubmodule LieSubmodule.top_toSubmodule LieSubalgebra.top_toSubmodule LieSubmodule.coe_lieSpan_submodule_eq_iff
isIdealMorphism_def 📖	mathematical	—	IsIdealMorphism LieIdeal.toLieSubalgebra idealRange range	—	—
isIdealMorphism_iff 📖	mathematical	—	IsIdealMorphism Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule DFunLike.coe LieHom instFunLike	—	—
isIdealMorphism_of_surjective 📖	mathematical	DFunLike.coe LieHom instFunLike	IsIdealMorphism	—	isIdealMorphism_def idealRange_eq_top_of_surjective range_eq_top LieIdeal.top_toLieSubalgebra
ker_eq_bot 📖	mathematical	—	ker Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule DFunLike.coe LieHom instFunLike	—	ker_toSubmodule LieSubmodule.bot_toSubmodule LinearMap.ker_eq_bot coe_toLinearMap
ker_le_comap 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule ker LieIdeal.comap	—	LieIdeal.comap_mono bot_le
ker_toSubmodule 📖	mathematical	—	LieSubmodule.toSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule ker LinearMap.ker CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring toLinearMap	—	—
le_ker_iff 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule ker DFunLike.coe LieHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	mem_ker
map_le_idealRange 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieIdeal.map idealRange	—	idealRange_eq_map LieIdeal.map_mono le_top
mem_idealRange 📖	mathematical	—	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule idealRange DFunLike.coe LieHom instFunLike	—	idealRange_eq_map LieIdeal.mem_map LieSubmodule.mem_top
mem_idealRange_iff 📖	mathematical	IsIdealMorphism	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule idealRange DFunLike.coe LieHom instFunLike	—	LieSubmodule.mem_coe LieIdeal.coe_toLieSubalgebra isIdealMorphism_def coe_range Set.mem_range
mem_ker 📖	mathematical	—	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule ker DFunLike.coe LieHom instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
range_eq_top 📖	mathematical	—	range Top.top LieSubalgebra LieSubalgebra.instTop DFunLike.coe LieHom instFunLike	—	RingHomSurjective.ids range_toSubmodule LieSubalgebra.top_toSubmodule LinearMap.range_eq_top
range_subset_idealRange 📖	mathematical	—	Set Set.instHasSubset SetLike.coe LieSubalgebra LieSubalgebra.instSetLike range LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule idealRange	—	LieSubmodule.subset_lieSpan
range_toSubmodule 📖	mathematical	—	LieSubalgebra.toSubmodule range LinearMap.range CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieRing.toAddCommGroup LieAlgebra.toModule RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids toLinearMap	—	—

LieHom.IsIdealMorphism

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq 📖	mathematical	LieHom.IsIdealMorphism	LieIdeal.toLieSubalgebra LieHom.idealRange LieHom.range	—	—

LieIdeal

Definitions

Name	Category	Theorems
comap 📖	CompOp	20 math math: comap_incl_eq_top, gc_map_comap, map_comap_incl, derivedSeries_eq_derivedSeriesOfIdeal_comap, comap_bracket_incl_of_le, LieHom.ker_le_comap, comap_bracket_le, comap_bracket_incl, map_comap_bracket_eq, comap_map_eq, comap_mono, comap_incl_self, map_comap_eq, comap_map_le, mem_comap, map_le_iff_le_comap, comap_bracket_eq, comap_incl_eq_bot, comap_toSubmodule, map_comap_le
incl 📖	CompOp	16 math math: derivedSeries_eq_derivedSeriesOfIdeal_map, comap_incl_eq_top, map_comap_incl, incl_injective, derivedSeries_eq_derivedSeriesOfIdeal_comap, comap_bracket_incl_of_le, incl_coe, incl_isIdealMorphism, incl_range, comap_bracket_incl, incl_idealRange, comap_incl_self, incl_apply, ker_incl, comap_incl_eq_bot, LieAlgebra.isExtension_of_surjective
inclusion 📖	CompOp	3 math math: coe_inclusion, inclusion_injective, inclusion_apply
lieAlgebra 📖	CompOp	38 math math: derivedSeries_eq_derivedSeriesOfIdeal_map, LieAlgebra.IsSemisimple.isSimple_of_isAtom, comap_incl_eq_top, restrict_killingForm, map_comap_incl, incl_injective, derivedSeries_eq_derivedSeriesOfIdeal_comap, LieSubmodule.traceForm_eq_of_le_idealizer, LieAlgebra.Extension.toKer_bracket, comap_bracket_incl_of_le, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, incl_coe, incl_isIdealMorphism, lieModule, subsingleton_of_bot, LieAlgebra.Extension.ringModuleOf_bracket, isLieAbelian_iff, incl_range, coe_inclusion, inclusion_injective, topEquiv_apply, derivedSeries_eq_bot_iff, comap_bracket_incl, killingForm_eq, incl_idealRange, comap_incl_self, LieAlgebra.Extension.ringModuleOf_bracket_proj, coe_lcs_eq, LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, LieAlgebra.Extension.twoCocycleOf_coe_coe, incl_apply, LieAlgebra.Extension.lie_toKer_apply, ker_incl, comap_incl_eq_bot, inclusion_apply, LieModule.coe_lowerCentralSeries_ideal_le, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieAlgebra.isExtension_of_surjective
lieRing 📖	CompOp	62 math math: derivedSeries_eq_derivedSeriesOfIdeal_map, LieAlgebra.abelian_radical_of_hasTrivialRadical, LieAlgebra.IsSemisimple.isSimple_of_isAtom, comap_incl_eq_top, restrict_killingForm, coe_bracket_of_module, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, map_comap_incl, incl_injective, derivedSeries_eq_derivedSeriesOfIdeal_comap, LieAlgebra.le_solvable_ideal_solvable, LieAlgebra.derivedSeries_of_derivedLength_succ, LieSubmodule.traceForm_eq_of_le_idealizer, LieAlgebra.Extension.toKer_bracket, instIsNilpotentSubtypeMemLieSubmoduleOfIsNilpotent, comap_bracket_incl_of_le, LieAlgebra.abelian_radical_iff_solvable_is_abelian, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, incl_coe, incl_isIdealMorphism, lieModule, subsingleton_of_bot, LieAlgebra.Extension.ringModuleOf_bracket, isLieAbelian_iff, LieAlgebra.abelian_iff_derived_one_eq_bot, incl_range, coe_inclusion, inclusion_injective, topEquiv_apply, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, derivedSeries_eq_bot_iff, comap_bracket_incl, killingForm_eq, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, incl_idealRange, comap_incl_self, LieAlgebra.radicalIsSolvable, isLieAbelian_of_trivial, LieAlgebra.Extension.ringModuleOf_bracket_proj, LieAlgebra.abelian_derivedAbelianOfIdeal, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, LieAlgebra.isSolvableAdd, LieAlgebra.maxNilpotentIdealIsNilpotent, coe_lcs_eq, LieAlgebra.derivedLength_eq_derivedLengthOfIdeal, instIsLieTowerSubtypeMemLieSubmodule, LieAlgebra.Extension.twoCocycleOf_coe_coe, LieAlgebra.isSolvableBot, LieAlgebra.LieIdeal.solvable_iff_le_radical, incl_apply, Function.instIsSolvableSubtypeMemLieSubmodule, LieAlgebra.Extension.lie_toKer_apply, ker_incl, comap_incl_eq_bot, inclusion_apply, LieModule.coe_lowerCentralSeries_ideal_le, LieAlgebra.Extension.oneCochainOfTwoSplitting_apply, LieAlgebra.isExtension_of_surjective
lieRingModule 📖	CompOp	22 math math: LieAlgebra.abelian_radical_of_hasTrivialRadical, restrict_killingForm, coe_bracket_of_module, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieAlgebra.derivedSeries_of_derivedLength_succ, LieSubmodule.traceForm_eq_of_le_idealizer, LieAlgebra.abelian_radical_iff_solvable_is_abelian, LieModule.instIsTriangularizableSubtypeMemLieSubmodule, lieModule, isLieAbelian_iff, LieAlgebra.abelian_iff_derived_one_eq_bot, LieAlgebra.IsSemisimple.non_abelian_of_isAtom, LieAlgebra.abelian_of_le_center, isLieAbelian_of_trivial, LieAlgebra.abelian_derivedAbelianOfIdeal, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieAlgebra.instIsLieAbelianSubtypeMemLieSubmoduleCenter, instIsLieTowerSubtypeMemLieSubmodule_1, LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieSubmoduleKerProj, coe_lcs_eq, instIsLieTowerSubtypeMemLieSubmodule, LieModule.coe_lowerCentralSeries_ideal_le
map 📖	CompOp	25 math math: derivedSeries_eq_derivedSeriesOfIdeal_map, map_bracket_le, derivedSeries_map_eq, gc_map_comap, map_comap_incl, lowerCentralSeries_map_eq, derivedSeries_map_le, map_of_image, map_mono, map_lowerCentralSeries_le, map_sup_ker_eq_map', coe_map_of_surjective, map_comap_bracket_eq, LieHom.idealRange_eq_map, map_comap_eq, comap_map_le, map_bracket_eq, map_le_iff_le_comap, LieHom.map_le_idealRange, map_le, map_sup_ker_eq_map, map_eq_bot_iff, map_comap_le, mem_map, map_sup
toLieSubalgebra 📖	CompOp	21 math math: restrict_killingForm, LieHom.isIdealMorphism_def, LieModule.lowerCentralSeries_one_inf_center_le_ker_traceForm, LieAlgebra.InvariantForm.restrict_nondegenerate, coe_killingCompl_top, LieSubmodule.traceForm_eq_of_le_idealizer, coe_toLieSubalgebra, incl_coe, LieHom.IsIdealMorphism.eq, LieSubalgebra.exists_nested_lieIdeal_coe_eq_iff, toLieSubalgebra_toSubmodule, incl_range, LieAlgebra.IsKilling.disjoint_ker_weight_corootSpace, LieAlgebra.InvariantForm.restrict_orthogonal_nondegenerate, killingForm_eq, LieSubalgebra.exists_lieIdeal_coe_eq_iff, normalizer_eq_top, top_toLieSubalgebra, LieAlgebra.IsExtension.exact, LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer, LieHom.range_eq_ker_iff
topEquiv 📖	CompOp	1 math math: topEquiv_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_of_map_eq_bot 📖	—	DFunLike.coe LieHom LieHom.instFunLike map Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	—	eq_bot_iff LieHom.ker.eq_1 LieHom.ker_eq_bot map_le_iff_le_comap
coe_bracket_of_module 📖	mathematical	—	Bracket.bracket LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket lieRing lieRingModule	—	LieSubalgebra.coe_bracket_of_module
coe_inclusion 📖	mathematical	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
coe_map_of_surjective 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike	LieSubmodule.toSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LieHom.toLinearMap	—	RingHomSurjective.ids Set.image_congr LieSubmodule.lie_mem LieHom.map_lie map.eq_1 toLieSubalgebra_toSubmodule LieSubmodule.coe_lieSpan_submodule_eq_iff
coe_toLieSubalgebra 📖	mathematical	—	SetLike.coe LieSubalgebra LieSubalgebra.instSetLike toLieSubalgebra LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	—
comap_incl_eq_bot 📖	mathematical	—	comap LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl Bot.bot LieIdeal LieSubmodule.instBot Disjoint LieSubmodule.instPartialOrder BoundedOrder.toOrderBot Preorder.toLE PartialOrder.toPreorder CompleteLattice.toBoundedOrder LieSubmodule.instCompleteLattice	—	disjoint_iff comap_toSubmodule LieSubmodule.bot_toSubmodule LieSubmodule.inf_toSubmodule incl_coe Submodule.disjoint_iff_comap_eq_bot
comap_incl_eq_top 📖	mathematical	—	comap LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl Top.top LieIdeal LieSubmodule.instTop Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder	—	comap_toSubmodule LieSubmodule.top_toSubmodule incl_coe Submodule.comap_subtype_eq_top LieSubmodule.toSubmodule_le_toSubmodule
comap_incl_self 📖	mathematical	—	comap LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl Top.top LieIdeal LieSubmodule.instTop	—	LieSubmodule.ext
comap_map_eq 📖	mathematical	SetLike.coe LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map Set.image DFunLike.coe LieHom LieHom.instFunLike	comap LieSubmodule.instMax LieHom.ker	—	comap_toSubmodule RingHomSurjective.ids map_toSubmodule LieSubmodule.sup_toSubmodule LieHom.ker_toSubmodule Submodule.comap_map_eq
comap_map_le 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule comap map	—	map_le_iff_le_comap le_refl
comap_mono 📖	mathematical	—	Monotone LieIdeal PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule comap	—	SetLike.coe_subset_coe instIsConcreteLE Set.preimage_mono
comap_toSubmodule 📖	mathematical	—	LieSubmodule.toSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule comap Submodule.comap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring LieHom.toLinearMap	—	—
gc_map_comap 📖	mathematical	—	GaloisConnection LieIdeal PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map comap	—	map_le_iff_le_comap
incl_apply 📖	mathematical	—	DFunLike.coe LieHom LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra LieHom.instFunLike incl	—	—
incl_coe 📖	mathematical	—	LieHom.toLinearMap LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl Submodule.subtype CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LieSubalgebra.toSubmodule toLieSubalgebra	—	—
incl_idealRange 📖	mathematical	—	LieHom.idealRange LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl	—	LieHom.idealRange_eq_lieSpan_range LieSubalgebra.coe_toSubmodule incl_range toLieSubalgebra_toSubmodule LieSubmodule.coe_lieSpan_submodule_eq_iff
incl_injective 📖	mathematical	—	LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike incl	—	Subtype.val_injective
incl_isIdealMorphism 📖	mathematical	—	LieHom.IsIdealMorphism LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl	—	LieHom.isIdealMorphism_def incl_idealRange LieSubalgebra.incl_range
incl_range 📖	mathematical	—	LieHom.range LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl toLieSubalgebra	—	LieSubalgebra.incl_range
inclusion_apply 📖	mathematical	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	DFunLike.coe LieHom LieSubmodule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
inclusion_injective 📖	mathematical	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	LieSubmodule SetLike.instMembership LieSubmodule.instSetLike DFunLike.coe LieHom lieRing lieAlgebra LieHom.instFunLike inclusion	—	—
ker_incl 📖	mathematical	—	LieHom.ker LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra incl Bot.bot LieIdeal LieSubmodule.instBot	—	LieSubmodule.ext AddSubmonoidClass.toZeroMemClass AddSubgroupClass.toAddSubmonoidClass LieSubmodule.instAddSubgroupClass
lieModule 📖	mathematical	—	LieModule LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike lieRing lieAlgebra lieRingModule	—	LieSubalgebra.lieModule
map_comap_eq 📖	mathematical	LieHom.IsIdealMorphism	map comap LieIdeal LieSubmodule.instMin LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieHom.idealRange	—	le_antisymm le_inf_iff LieHom.map_le_idealRange map_comap_le SetLike.coe_subset_coe instIsConcreteLE LieSubmodule.coe_inf coe_toLieSubalgebra LieHom.isIdealMorphism_def mem_map
map_comap_le 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map comap	—	map_le_iff_le_comap le_refl
map_eq_bot_iff 📖	mathematical	—	map Bot.bot LieIdeal LieSubmodule.instBot LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieHom.ker	—	le_bot_iff map_le_iff_le_comap
map_le 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map Set Set.instHasSubset Set.image DFunLike.coe LieHom LieHom.instFunLike SetLike.coe LieSubmodule.instSetLike	—	LieSubmodule.lieSpan_le
map_le_iff_le_comap 📖	mathematical	—	LieIdeal Preorder.toLE PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map comap	—	map_le Set.image_subset_iff
map_mono 📖	mathematical	—	Monotone LieIdeal PartialOrder.toPreorder LieSubmodule.instPartialOrder LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map	—	LieSubmodule.lieSpan_mono instIsConcreteLE Submodule.map_mono
map_of_image 📖	mathematical	Set.image DFunLike.coe LieHom LieHom.instFunLike SetLike.coe LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	map	—	le_antisymm map.eq_1 LieSubmodule.lieSpan_le Submodule.map_coe subset_refl Set.instReflSubset SetLike.coe_subset_coe instIsConcreteLE LieSubmodule.subset_lieSpan
map_sup 📖	mathematical	—	map LieIdeal LieSubmodule.instMax LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	GaloisConnection.l_sup gc_map_comap
map_sup_ker_eq_map 📖	mathematical	—	map LieIdeal LieSubmodule.instMax LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieHom.ker	—	le_antisymm LieSubmodule.lieSpan_mono LieSubmodule.mem_sup map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass LieHom.coe_toLinearMap LieHom.mem_ker add_zero map_mono le_sup_left
map_sup_ker_eq_map' 📖	mathematical	—	LieIdeal LieSubmodule.instMax LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map LieHom.ker	—	map_sup map_sup_ker_eq_map
map_toSubmodule 📖	mathematical	SetLike.coe LieIdeal LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map Set.image DFunLike.coe LieHom LieHom.instFunLike	LieSubmodule.toSubmodule Submodule.map CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LieHom.toLinearMap	—	RingHomSurjective.ids SetLike.ext'_iff LieSubmodule.coe_toSubmodule Submodule.map_coe
mem_comap 📖	mathematical	—	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule comap DFunLike.coe LieHom LieHom.instFunLike	—	—
mem_map 📖	mathematical	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	map DFunLike.coe LieHom LieHom.instFunLike	—	LieSubmodule.subset_lieSpan
mem_map_of_surjective 📖	mathematical	DFunLike.coe LieHom LieHom.instFunLike LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule map	LieSubmodule	—	RingHomSurjective.ids Submodule.mem_map coe_map_of_surjective LieSubmodule.mem_toSubmodule LieHom.coe_toLinearMap
subsingleton_of_bot 📖	mathematical	—	LieIdeal LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike Bot.bot LieSubmodule.instBot lieRing lieAlgebra	—	subsingleton_of_bot_eq_top LieSubmodule.subsingleton_of_bot
toLieSubalgebra_toSubmodule 📖	mathematical	—	LieSubalgebra.toSubmodule toLieSubalgebra LieSubmodule.toSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	—	—
topEquiv_apply 📖	mathematical	—	DFunLike.coe LieEquiv LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike Top.top LieIdeal LieSubmodule.instTop lieRing lieAlgebra EquivLike.toFunLike LieEquiv.instEquivLike topEquiv	—	—
top_toLieSubalgebra 📖	mathematical	—	toLieSubalgebra Top.top LieIdeal LieSubmodule.instTop LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule LieSubalgebra LieSubalgebra.instTop	—	—

LieSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_lieIdeal_coe_eq_iff 📖	mathematical	—	LieIdeal.toLieSubalgebra LieSubalgebra SetLike.instMembership instSetLike Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule	—	Submodule.exists_lieSubmodule_coe_eq_iff
exists_nested_lieIdeal_coe_eq_iff 📖	mathematical	LieSubalgebra Preorder.toLE PartialOrder.toPreorder instPartialOrder_1	LieIdeal.toLieSubalgebra SetLike.instMembership instSetLike lieRing lieAlgebra ofLe Bracket.bracket LieRingModule.toBracket LieRing.toAddCommGroup lieRingSelfModule	—	—

(root)

Definitions

Name	Category	Theorems
LieIdeal 📖	CompOp	146 math math: LieAlgebra.Extension.incl_apply_mem_ker, LieIdeal.map_bracket_le, LieSubmodule.lie_sup, LieIdeal.comap_incl_eq_top, LieAlgebra.derivedLength_zero, LieAlgebra.isSolvable_iff_int, LieModule.derivedSeries_le_lowerCentralSeries, LieHom.mem_idealRange, LieSubmodule.bot_lie, LieIdeal.gc_map_comap, LieSubmodule.lie_abelian_iff_lie_self_eq_bot, LieIdeal.map_comap_incl, LieAlgebra.hasTrivialRadical_iff, LieAlgebra.IsKilling.corootSpace_eq_bot_iff, LieAlgebra.IsSemisimple.booleanGenerators, LieSubmodule.lie_le_iff, LieAlgebra.derivedSeriesOfIdeal_succ_le, LieSubmodule.comap_bracket_eq, LieSubmodule.lieIdeal_oper_eq_linear_span', LieHom.quotKerEquivRange_toFun, LieIdeal.coe_killingCompl_top, LieSubmodule.lie_bot, LieIdeal.coe_toLieSubalgebra, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieSubmodule.lie_inf, LieAlgebra.abelian_of_solvable_ideal_eq_bot_iff, LieIdeal.mem_killingCompl, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.sup_lie, LieModule.mem_ker, LieIdeal.le_killingCompl_top_of_isLieAbelian, LieAlgebra.Extension.lie_incl_mem_ker, LieAlgebra.radical_eq_top_of_isSolvable, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_top, LieIdeal.derivedSeries_map_le, LieHom.ker_eq_bot, LieModule.lowerCentralSeries_succ, LieSubmodule.lie_le_inf, LieAlgebra.derivedSeriesOfIdeal_le_self, LieIdeal.subsingleton_of_bot, LieAlgebra.isSolvable_iff, LieAlgebra.derivedSeriesOfIdeal_succ, LieAlgebra.IsSemisimple.sSup_atoms_eq_top, LieAlgebra.IsSimple.isAtom_top, LieIdeal.lcs_succ, LieIdeal.isLieAbelian_iff, LieSubmodule.trivial_lie_oper_zero, LieAlgebra.IsKilling.coroot_mem_corootSpace, LieAlgebra.abelian_iff_derived_one_eq_bot, LieIdeal.map_mono, LieSubmodule.lie_comm, LieAlgebra.center_le_radical, LieSubmodule.mono_lie_right, coe_lowerCentralSeries_ideal_quot_eq, LieHom.ker_le_comap, LieIdeal.comap_bracket_le, LieIdeal.map_lowerCentralSeries_le, LieAlgebra.hasTrivialRadical_iff_no_solvable_ideals, LieIdeal.map_sup_ker_eq_map', LieAlgebra.derivedSeriesOfIdeal_antitone, LieSubmodule.lie_baseChange, LieAlgebra.IsExtension.ker_eq_bot, LieSubmodule.top_lie_le_iff_le_normalizer, LieIdeal.topEquiv_apply, LieAlgebra.IsSolvable.solvable_int, LieAlgebra.derivedSeriesOfIdeal_add_le_add, LieModule.ideal_oper_maxTrivSubmodule_eq_bot, LieAlgebra.derivedSeries_def, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_top_iff, LieAlgebra.IsKilling.biSup_corootSpace_eq_top, LieIdeal.isCompl_killingCompl, LieHom.quotKerEquivRange_invFun, LieAlgebra.LieIdeal.isNilpotent_iff_le_maxNilpotentIdeal, LieIdeal.derivedSeries_eq_bot_iff, LieIdeal.comap_bracket_incl, LieSubmodule.mem_idealizer, LieAlgebra.center_eq_bot, LieModule.isFaithful_iff_ker_eq_bot, LieAlgebra.isLieAbelian_iff_center_eq_top, LieIdeal.coe_derivedSeries_eq_int, LieIdeal.map_comap_bracket_eq, LieHom.idealRange_eq_map, LieModule.le_max_triv_iff_bracket_eq_bot, LieIdeal.comap_mono, LieAlgebra.IsKilling.ideal_eq_bot_of_isLieAbelian, LieSubmodule.inf_lie, LieAlgebra.HasTrivialRadical.radical_eq_bot, LieSubmodule.lie_le_right, LieIdeal.comap_incl_self, LieAlgebra.IsKilling.cartanEquivDual_symm_apply_mem_corootSpace, LieHom.mem_ker, LieAlgebra.IsKilling.killingCompl_top_eq_bot, LieIdeal.map_comap_eq, LieIdeal.comap_map_le, LieAlgebra.hasTrivialRadical_iff_no_abelian_ideals, LieAlgebra.isFaithful_self_iff, LieHom.range_subset_idealRange, LieIdeal.mem_comap, LieIdeal.map_bracket_eq, LieSubmodule.lieIdeal_oper_eq_tensor_map_range, LieIdeal.map_le_iff_le_comap, LieIdeal.top_toLieSubalgebra, LieSubmodule.lieIdeal_oper_eq_linear_span, LieAlgebra.mem_corootSpace', LieAlgebra.derivedSeries_lt_top_of_solvable, LieIdeal.derivedSeries_succ_eq_top_iff, LieAlgebra.derivedSeries_of_bot_eq_bot, LieAlgebra.IsKilling.invtSubmoduleToLieIdeal_apply_eq_bot_iff, LieHom.map_le_idealRange, LieSubmodule.lieIdeal_oper_eq_span, LieAlgebra.abelian_iff_derived_succ_eq_bot, LieIdeal.map_le, LieSubmodule.exists_smul_add_of_span_sup_eq_top, LieAlgebra.center_le_maxNilpotentIdeal, LieSubmodule.lcs_succ, LieHom.mem_idealRange_iff, LieAlgebra.mem_corootSpace, LieAlgebra.isSolvableAdd, LieAlgebra.HasTrivialRadical.eq_bot_of_isSolvable, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LieAlgebra.InvariantForm.atomistic, LieDerivation.mem_ad_idealRange_iff, LieHom.le_ker_iff, LieAlgebra.IsSemisimple.sSupIndep_isAtom, LieSubmodule.map_bracket_eq, LieAlgebra.isSolvableBot, LieIdeal.comap_bracket_eq, LieAlgebra.LieIdeal.solvable_iff_le_radical, LieAlgebra.IsSolvable.solvable, LieIdeal.map_sup_ker_eq_map, LieAlgebra.IsSimple.isAtom_iff_eq_top, LieAlgebra.IsKilling.corootSpace_zero_eq_bot, LieSubmodule.lie_eq_bot_iff, LieIdeal.ker_incl, LieSubmodule.lie_le_left, LieIdeal.lcs_top, LieIdeal.comap_incl_eq_bot, LieIdeal.map_eq_bot_iff, lie_eq_self_of_isAtom_of_ne_bot, LieSubmodule.lie_coe_mem_lie, LieIdeal.map_comap_le, LieAlgebra.IsSimple.eq_bot_or_eq_top, LieModule.ker_eq_bot, LieIdeal.map_sup, LieHom.idealRange_eq_top_of_surjective, LieSubmodule.gc_top_lie_normalizer
instCoeLieIdealLieSubalgebra 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsLieTowerSubtypeMemLieSubmodule 📖	mathematical	—	IsLieTower LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket LieIdeal.lieRing LieIdeal.lieRingModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	leibniz_lie instIsLieTower
instIsLieTowerSubtypeMemLieSubmodule_1 📖	mathematical	—	IsLieTower LieSubmodule LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule SetLike.instMembership LieSubmodule.instSetLike LieRingModule.toBracket AddSubgroupClass.toAddCommGroup LieSubmodule.instAddSubgroupClass LieSubmodule.instLieRingModuleSubtypeMem LieIdeal.lieRing LieIdeal.lieRingModule AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid	—	LieSubmodule.instAddSubgroupClass leibniz_lie instIsLieTower
lie_mem_left 📖	mathematical	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	Bracket.bracket LieRingModule.toBracket	—	lie_skew neg_lie lie_mem_right
lie_mem_right 📖	mathematical	LieIdeal SetLike.instMembership LieSubmodule.instSetLike LieRing.toAddCommGroup LieAlgebra.toModule lieRingSelfModule	Bracket.bracket LieRingModule.toBracket	—	LieSubmodule.lie_mem

---

← Back to Index