Documentation Verification Report

EngelSubalgebra

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

Statistics

Metric	Count
Definitions `engel`	1
Theorems `engel_carrier`, `engel_zero`, `isNilpotent_of_forall_le_engel`, `mem_engel_iff`, `normalizer_engel`, `normalizer_eq_self_of_engel_le`, `self_mem_engel`	7
Total	8

LieSubalgebra

Definitions

Name	Category	Theorems
`engel` 📖	CompOp	10 math math: `LieAlgebra.finrank_engel`, `LieAlgebra.exists_isCartanSubalgebra_engel_of_finrank_le_card`, `normalizer_engel`, `engel_carrier`, `self_mem_engel`, `mem_engel_iff`, `LieAlgebra.exists_isCartanSubalgebra_engel`, `engel_zero`, `LieAlgebra.rank_le_finrank_engel`, `LieAlgebra.isRegular_iff_finrank_engel_eq_rank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`engel_carrier` 📖	mathematical	—	`SetLike.coe` `LieSubalgebra` `instSetLike` `engel` `Set.iInter` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `Submodule.setLike`	—	`Set.iInter_congr_Prop` `iSup_congr_Prop` `zero_smul` `smulCommClass_self` `sub_zero` `iSup_pos`
`engel_zero` 📖	mathematical	—	`engel` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup` `Top.top` `LieSubalgebra` `instTop`	—	`eq_top_iff` `smulCommClass_self` `IsScalarTower.left` `mem_engel_iff` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass` `pow_one`
`isNilpotent_of_forall_le_engel` 📖	mathematical	`LieSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder_1` `engel`	`LieRing.IsNilpotent` `SetLike.instMembership` `instSetLike` `lieRing`	—	`smulCommClass_self` `IsScalarTower.left` `LieAlgebra.isNilpotent_iff_forall` `instIsNoetherianSubtypeMem` `LinearMap.mem_ker` `Module.End.pow_map_zero_of_le` `monotone_stabilizes_iff_noetherian` `LinearMap.ext` `coe_ad_pow` `mem_engel_iff` `le_total`
`mem_engel_iff` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `engel` `DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toNatPow` `Module.End.instMonoid` `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` `LieAlgebra.ad` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid`	—	`smulCommClass_self` `IsScalarTower.left` `Module.End.mem_maxGenEigenspace` `zero_smul` `sub_zero`
`normalizer_engel` 📖	mathematical	—	`normalizer` `engel`	—	`le_antisymm` `smulCommClass_self` `IsScalarTower.left` `mem_engel_iff` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `lie_skew` `mem_normalizer_iff` `self_mem_engel` `pow_succ` `Module.End.mul_apply` `le_normalizer`
`normalizer_eq_self_of_engel_le` 📖	mathematical	`LieSubalgebra` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder_1` `engel`	`normalizer`	—	`le_antisymm` `lie_skew` `neg_mem_iff` `AddSubgroupClass.toNegMemClass` `instAddSubgroupClass` `mem_normalizer_iff` `self_mem_engel` `le_normalizer` `IsScalarTower.left` `smulCommClass_self` `RingHomSurjective.ids` `Filter.eventually_atTop` `instIsDirectedOrder` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `instArchimedeanNat` `LinearMap.eventually_codisjoint_ker_pow_range_pow` `instIsArtinianSubtypeMem` `Submodule.map_subtype_top` `Submodule.map_le_iff_le_comap` `le_sup_of_le_left` `pow_zero` `AddSubmonoid.mk_eq_zero` `le_sup_of_le_right` `pow_succ'` `sup_eq_right`
`self_mem_engel` 📖	mathematical	—	`LieSubalgebra` `SetLike.instMembership` `instSetLike` `engel`	—	`smulCommClass_self` `IsScalarTower.left` `pow_one` `lie_self`

---

← Back to Index