IdealOperations

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

Statistics

Metric	Count
Definitions `hasBracket`	1
Theorems `comap_bracket_eq`, `comap_bracket_incl`, `comap_bracket_incl_of_le`, `comap_bracket_le`, `map_bracket_eq`, `map_bracket_le`, `map_comap_bracket_eq`, `map_comap_incl`, `bot_lie`, `comap_bracket_eq`, `comap_map_eq`, `inf_lie`, `le_comap_map`, `lieIdeal_oper_eq_linear_span`, `lieIdeal_oper_eq_linear_span'`, `lieIdeal_oper_eq_span`, `lie_bot`, `lie_coe_mem_lie`, `lie_comm`, `lie_eq_bot_iff`, `lie_inf`, `lie_le_iff`, `lie_le_inf`, `lie_le_left`, `lie_le_right`, `lie_mem_lie`, `lie_sup`, `map_bracket_eq`, `map_comap_eq`, `map_comap_incl`, `map_comap_le`, `mono_lie`, `mono_lie_left`, `mono_lie_right`, `sup_lie`	35
Total	36

LieIdeal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comap_bracket_eq` 📖	mathematical	`LieHom.IsIdealMorphism`	`comap` `Bracket.bracket` `LieIdeal` `LieSubmodule.hasBracket` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieSubmodule.instMin` `LieHom.idealRange` `LieSubmodule.instMax` `LieHom.ker`	—	`comap_toSubmodule` `LieSubmodule.sup_toSubmodule` `LieHom.ker_toSubmodule` `RingHomSurjective.ids` `Submodule.comap_map_eq` `LieSubmodule.lieIdeal_oper_eq_linear_span` `lieAlgebraSelfModule` `LinearMap.map_span` `LieHom.map_lie`
`comap_bracket_incl` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `LieSubmodule.hasBracket` `comap` `incl` `LieSubmodule.instMin`	—	`incl_idealRange` `comap_bracket_eq` `incl_isIdealMorphism` `ker_incl` `sup_bot_eq`
`comap_bracket_incl_of_le` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	`Bracket.bracket` `LieSubmodule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `LieSubmodule.hasBracket` `comap` `incl`	—	`comap_bracket_incl` `inf_eq_right`
`comap_bracket_le` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Bracket.bracket` `LieSubmodule.hasBracket` `comap`	—	`map_le_iff_le_comap` `le_trans` `map_bracket_le` `LieSubmodule.mono_lie` `map_comap_le`
`map_bracket_eq` 📖	mathematical	`DFunLike.coe` `LieHom` `LieHom.instFunLike`	`map` `Bracket.bracket` `LieIdeal` `LieSubmodule.hasBracket` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`LieSubmodule.toSubmodule_le_toSubmodule` `RingHomSurjective.ids` `coe_map_of_surjective` `LieSubmodule.lieIdeal_oper_eq_linear_span` `lieAlgebraSelfModule` `LinearMap.map_span` `Submodule.span_mono` `mem_map_of_surjective` `LieHom.map_lie` `le_antisymm` `map_bracket_le`
`map_bracket_le` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubmodule.instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `map` `Bracket.bracket` `LieSubmodule.hasBracket`	—	`map_le_iff_le_comap` `LieSubmodule.lieIdeal_oper_eq_span` `LieSubmodule.lieSpan_le` `mem_map` `LieHom.map_lie` `LieSubmodule.lie_coe_mem_lie`
`map_comap_bracket_eq` 📖	mathematical	`LieHom.IsIdealMorphism`	`map` `Bracket.bracket` `LieIdeal` `LieSubmodule.hasBracket` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `comap` `LieSubmodule.instMin` `LieHom.idealRange`	—	`map_sup_ker_eq_map` `comap_bracket_eq` `map_comap_eq` `inf_eq_right` `le_trans` `LieSubmodule.lie_le_left` `inf_le_left`
`map_comap_incl` 📖	mathematical	—	`map` `LieSubmodule` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `LieSubmodule.instSetLike` `lieRing` `lieAlgebra` `incl` `comap` `LieIdeal` `LieSubmodule.instMin`	—	`incl_idealRange` `map_comap_eq` `incl_isIdealMorphism`

LieSubmodule

Definitions

Name	Category	Theorems
`hasBracket` 📖	CompOp	44 math math: `LieIdeal.map_bracket_le`, `lie_sup`, `bot_lie`, `lie_abelian_iff_lie_self_eq_bot`, `lie_le_iff`, `comap_bracket_eq`, `lieIdeal_oper_eq_linear_span'`, `lie_bot`, `LieIdeal.comap_bracket_incl_of_le`, `lie_top_eq_of_span_sup_eq_top`, `lie_inf`, `sup_lie`, `LieModule.lowerCentralSeries_succ`, `lie_le_inf`, `LieAlgebra.derivedSeriesOfIdeal_succ`, `LieIdeal.lcs_succ`, `trivial_lie_oper_zero`, `mono_lie_left`, `lie_comm`, `mono_lie_right`, `LieIdeal.comap_bracket_le`, `lie_baseChange`, `top_lie_le_iff_le_normalizer`, `LieModule.ideal_oper_maxTrivSubmodule_eq_bot`, `LieIdeal.comap_bracket_incl`, `lie_eq_self_of_isAtom_of_nonabelian`, `lie_mem_lie`, `LieIdeal.map_comap_bracket_eq`, `mono_lie`, `LieModule.le_max_triv_iff_bracket_eq_bot`, `inf_lie`, `lie_le_right`, `LieIdeal.map_bracket_eq`, `lieIdeal_oper_eq_tensor_map_range`, `lieIdeal_oper_eq_linear_span`, `lieIdeal_oper_eq_span`, `lcs_succ`, `map_bracket_eq`, `LieIdeal.comap_bracket_eq`, `lie_eq_bot_iff`, `lie_le_left`, `lie_eq_self_of_isAtom_of_ne_bot`, `lie_coe_mem_lie`, `gc_top_lie_normalizer`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lie` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `Bot.bot` `instBot` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`lieIdeal_oper_eq_span` `lieSpan_le` `mem_bot` `zero_lie` `le_bot_iff`
`comap_bracket_eq` 📖	mathematical	`LieModuleHom.ker` `Bot.bot` `LieSubmodule` `instBot` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieModuleHom.range`	`comap` `Bracket.bracket` `LieIdeal` `hasBracket`	—	`map_comap_eq` `map_bracket_eq` `comap_map_eq`
`comap_map_eq` 📖	mathematical	`LieModuleHom.ker` `Bot.bot` `LieSubmodule` `instBot`	`comap` `map`	—	`SetLike.ext'_iff` `Set.preimage_image_eq` `LieModuleHom.ker_eq_bot`
`inf_lie` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket` `instMin` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`le_inf_iff` `mono_lie_left` `inf_le_left` `inf_le_right`
`le_comap_map` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `comap` `map`	—	`Set.subset_preimage_image`
`lieIdeal_oper_eq_linear_span` 📖	mathematical	—	`toSubmodule` `Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `instSetLike` `LieRingModule.toBracket`	—	`le_antisymm` `Submodule.span_induction` `leibniz_lie` `instIsLieTower` `Submodule.add_mem` `Submodule.subset_span` `lie_mem` `lie_zero` `lie_add` `lie_smul` `Submodule.smul_mem` `lieIdeal_oper_eq_span` `lieSpan_le` `submodule_span_le_lieSpan`
`lieIdeal_oper_eq_linear_span'` 📖	mathematical	—	`toSubmodule` `Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `Submodule.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `SetLike.instMembership` `instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieRingModule.toBracket`	—	`lieIdeal_oper_eq_linear_span`
`lieIdeal_oper_eq_span` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `lieSpan` `setOf` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `SetLike.instMembership` `instSetLike` `LieRingModule.toBracket`	—	—
`lie_bot` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `Bot.bot` `instBot`	—	`eq_bot_iff` `lie_le_right`
`lie_coe_mem_lie` 📖	mathematical	—	`LieSubmodule` `SetLike.instMembership` `instSetLike` `Bracket.bracket` `LieIdeal` `hasBracket` `LieRingModule.toBracket` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`lieIdeal_oper_eq_span` `subset_lieSpan`
`lie_comm` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `hasBracket` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`lieIdeal_oper_eq_span` `lieSpan_le` `lie_skew` `lie_neg` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `coe_neg` `lie_coe_mem_lie` `le_antisymm`
`lie_eq_bot_iff` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `Bot.bot` `instBot` `LieRingModule.toBracket` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`lieIdeal_oper_eq_span` `lieSpan_eq_bot_iff`
`lie_inf` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket` `instMin`	—	`le_inf_iff` `mono_lie_right` `inf_le_left` `inf_le_right`
`lie_le_iff` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket` `SetLike.instMembership` `instSetLike` `LieRingModule.toBracket`	—	`lieIdeal_oper_eq_span` `lieSpan_le`
`lie_le_inf` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Bracket.bracket` `hasBracket` `instMin`	—	`le_inf_iff` `lie_le_left` `lie_le_right`
`lie_le_left` 📖	mathematical	—	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `Bracket.bracket` `hasBracket`	—	`lie_comm` `lie_le_right`
`lie_le_right` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `Bracket.bracket` `LieIdeal` `hasBracket`	—	`lieIdeal_oper_eq_span` `lieSpan_le` `lie_mem`
`lie_mem_lie` 📖	mathematical	`LieIdeal` `SetLike.instMembership` `instSetLike` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieSubmodule`	`Bracket.bracket` `hasBracket` `LieRingModule.toBracket`	—	`lie_coe_mem_lie`
`lie_sup` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `instMax`	—	`sup_le_iff` `mono_lie_right` `le_sup_left` `le_sup_right` `lieIdeal_oper_eq_span` `lieSpan_le` `mem_sup` `lie_coe_mem_lie` `lie_add` `le_antisymm`
`map_bracket_eq` 📖	mathematical	—	`map` `Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket`	—	`RingHomSurjective.ids` `toSubmodule_map` `lieIdeal_oper_eq_linear_span` `Submodule.map_span` `Set.ext` `Set.image_congr` `LieModuleHom.map_lie`
`map_comap_eq` 📖	mathematical	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieModuleHom.range`	`map` `comap`	—	`SetLike.ext'_iff` `Set.image_preimage_eq_of_subset`
`map_comap_incl` 📖	mathematical	—	`map` `LieSubmodule` `SetLike.instMembership` `instSetLike` `AddSubgroupClass.toAddCommGroup` `instAddSubgroupClass` `SubmoduleClass.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `AddCommGroup.toAddGroup` `instSMulMemClass` `instLieRingModuleSubtypeMem` `incl` `comap` `instMin`	—	`instAddSubgroupClass` `instSMulMemClass` `Submodule.map_comap_subtype`
`map_comap_le` 📖	mathematical	—	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `map` `comap`	—	`Set.image_preimage_subset`
`mono_lie` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule` `LieSubmodule`	`Bracket.bracket` `hasBracket`	—	`lieIdeal_oper_eq_span` `mem_lieSpan`
`mono_lie_left` 📖	mathematical	`LieIdeal` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	`LieSubmodule` `Bracket.bracket` `hasBracket`	—	`mono_lie` `le_refl`
`mono_lie_right` 📖	mathematical	`LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder`	`Bracket.bracket` `LieIdeal` `hasBracket`	—	`mono_lie` `le_refl`
`sup_lie` 📖	mathematical	—	`Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `instMax` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `lieRingSelfModule`	—	`sup_le_iff` `mono_lie_left` `le_sup_left` `le_sup_right` `lieIdeal_oper_eq_span` `lieSpan_le` `mem_sup` `lie_coe_mem_lie` `add_lie` `le_antisymm`

---

← Back to Index