Documentation Verification Report

Engel

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

Statistics

Metric	Count
Definitions `IsEngelian`	1
Theorems `isEngelian`, `exists_engelian_lieSubalgebra_of_lt_normalizer`, `isEngelian_of_isNoetherian`, `isEngelian_of_subsingleton`, `isNilpotent_iff_forall`, `isEngelian_iff`, `isNilpotent_iff_forall`, `isNilpotent_iff_forall'`, `exists_smul_add_of_span_sup_eq_top`, `isNilpotentOfIsNilpotentSpanSupEqTop`, `lcs_le_lcs_of_is_nilpotent_span_sup_eq_top`, `lie_top_eq_of_span_sup_eq_top`	12
Total	13

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEngelian` 📖	—	`DFunLike.coe` `LieHom` `LieHom.instFunLike` `LieAlgebra.IsEngelian`	—	—	`smulCommClass_self` `IsScalarTower.left` `LieModule.compLieHom` `lieModuleIsNilpotent`

LieAlgebra

Definitions

Name	Category	Theorems
`IsEngelian` 📖	MathDef	3 math math: `LieEquiv.isEngelian_iff`, `isEngelian_of_isNoetherian`, `isEngelian_of_subsingleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_engelian_lieSubalgebra_of_lt_normalizer` 📖	—	`IsEngelian` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.lieRing` `LieSubalgebra.lieAlgebra` `Preorder.toLT` `PartialOrder.toPreorder` `LieSubalgebra.instPartialOrder_1` `LieSubalgebra.normalizer`	—	—	`SetLike.exists_of_lt` `instIsConcreteLE` `LieSubalgebra.lie_mem_sup_of_mem_normalizer` `Submodule.mem_sup_left` `Submodule.subset_span` `Set.mem_singleton` `LieSubalgebra.toSubmodule_le_toSubmodule` `le_sup_right` `sup_le` `Submodule.span_singleton_le_iff_mem` `LT.lt.le` `LieSubalgebra.exists_nested_lieIdeal_ofLe_normalizer` `IsScalarTower.left` `LieIdeal.toLieSubalgebra_toSubmodule` `Submodule.map_injective_of_injective` `RingHomSurjective.ids` `Submodule.injective_subtype` `Submodule.map_sup` `Submodule.map_subtype_range_inclusion` `Submodule.map_top` `Submodule.range_subtype` `Submodule.map_subtype_span_singleton` `LieSubalgebra.coe_set_eq` `LieEquiv.isEngelian_iff` `LieSubmodule.isNilpotentOfIsNilpotentSpanSupEqTop` `LieIdeal.lieModule` `lt_iff_le_and_ne`
`isEngelian_of_isNoetherian` 📖	mathematical	—	`IsEngelian`	—	`smulCommClass_self` `IsScalarTower.left` `LieModule.isNilpotent_range_toEnd_iff` `isEngelian_of_subsingleton` `LieSubalgebra.subsingleton_bot` `exists_engelian_lieSubalgebra_of_lt_normalizer` `lt_of_le_of_ne` `LieSubalgebra.le_normalizer` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `LieSubmodule.Quotient.lieQuotientLieModule` `LieSubalgebra.normalizer_eq_self_iff` `LieSubmodule.nontrivial_iff_ne_bot` `Submodule.Quotient.nontrivial_iff` `isNilpotent_ad_of_isNilpotent` `Module.End.IsNilpotent.mapQ` `LieSubalgebra.lie_mem` `Subtype.prop` `LieModule.nontrivial_max_triv_of_isNilpotent` `WellFounded.has_min` `IsWellFounded.wf` `LieSubalgebra.wellFoundedGT_of_noetherian` `isNoetherian_of_surjective` `LinearMap.instIsScalarTower` `RingHomSurjective.ids` `LieHom.surjective_rangeRestrict` `LieModule.isNilpotent_of_top_iff` `Module.End.instLieModule` `LieModule.toEnd_module_end`
`isEngelian_of_subsingleton` 📖	mathematical	—	`IsEngelian`	—	`LieModule.lowerCentralSeries_succ` `LieSubmodule.trivial_lie_oper_zero` `LieModule.instIsTrivialOfSubsingleton`
`isNilpotent_iff_forall` 📖	mathematical	—	`LieRing.IsNilpotent` `IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `DFunLike.coe` `LieHom` `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` `LieHom.instFunLike` `ad`	—	`LieModule.isNilpotent_iff_forall` `lieAlgebraSelfModule`

LieEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isEngelian_iff` 📖	mathematical	—	`LieAlgebra.IsEngelian`	—	`Function.Surjective.isEngelian` `surjective`

LieModule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_iff_forall` 📖	mathematical	—	`IsNilpotent` `IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `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` `isNilpotent_toEnd_of_isNilpotent` `LieAlgebra.isEngelian_of_isNoetherian`
`isNilpotent_iff_forall'` 📖	mathematical	—	`IsNilpotent` `IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `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` `isNilpotent_range_toEnd_iff` `LieSubalgebra.lieModule` `Module.End.instLieModule` `isNilpotent_iff_forall` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_linearMap` `Module.IsNoetherian.finite` `toEnd_module_end`

LieSubmodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_smul_add_of_span_sup_eq_top` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `Top.top` `Submodule.instTop`	`LieIdeal` `SetLike.instMembership` `instSetLike` `lieRingSelfModule` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Module.toDistribMulAction`	—	`Submodule.mem_top`
`isNilpotentOfIsNilpotentSpanSupEqTop` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `Top.top` `Submodule.instTop` `IsNilpotent` `Module.End` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `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` `LieModule.toEnd`	`LieModule.IsNilpotent`	—	`smulCommClass_self` `IsScalarTower.left` `LieModule.IsNilpotent.nilpotent` `LieIdeal.lieModule` `LieIdeal.coe_lcs_eq` `MulZeroClass.zero_mul` `lcs_le_lcs_of_is_nilpotent_span_sup_eq_top` `LieModule.isNilpotent_iff`
`lcs_le_lcs_of_is_nilpotent_span_sup_eq_top` 📖	—	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `Top.top` `Submodule.instTop` `Module.End` `Monoid.toNatPow` `Module.End.instMonoid` `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` `LieModule.toEnd` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `LieSubmodule` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `LieModule.lowerCentralSeries` `LieIdeal.lcs`	—	—	`smulCommClass_self` `IsScalarTower.left` `RingHomSurjective.ids` `add_zero` `Submodule.map.congr_simp` `pow_zero` `Submodule.map_id` `LieIdeal.lcs_succ` `le_sup_of_le_left` `lie_top_eq_of_span_sup_eq_top` `LE.le.trans` `Submodule.map_mono` `Submodule.map_sup` `RingHomCompTriple.ids` `Submodule.map_comp` `Module.End.mul_eq_comp` `pow_succ'` `le_imp_le_of_le_of_le` `sup_le_sup` `le_refl` `coe_map_toEnd_le` `le_sup_of_le_right` `mono_lie` `le_trans` `LieModule.antitone_lowerCentralSeries` `le_self_add` `Nat.instCanonicallyOrderedAdd` `Submodule.map_zero` `bot_sup_eq`
`lie_top_eq_of_span_sup_eq_top` 📖	mathematical	`Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.span` `Set` `Set.instSingletonSet` `LieSubalgebra.toSubmodule` `LieIdeal.toLieSubalgebra` `Top.top` `Submodule.instTop`	`toSubmodule` `Bracket.bracket` `LieIdeal` `LieSubmodule` `hasBracket` `instTop` `lieRingSelfModule` `Submodule.map` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `DFunLike.coe` `LieHom` `Module.End` `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` `LieModule.toEnd`	—	`RingHomSurjective.ids` `smulCommClass_self` `IsScalarTower.left` `lieIdeal_oper_eq_linear_span'` `Submodule.sup_span` `Set.image_congr` `le_antisymm` `Submodule.span_le` `exists_smul_add_of_span_sup_eq_top` `Submodule.span_union` `Submodule.subset_span` `Submodule.smul_mem'` `lie_smul` `add_lie` `smul_lie` `Submodule.span_mono`

---

← Back to Index