Documentation Verification Report

CartanExists

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

Statistics

Metric	Count
Definitions	0
Theorems `engel_isBot_of_isMin`, `lieCharpoly_coeff_natDegree`, `lieCharpoly_map_eval`, `lieCharpoly_monic`, `lieCharpoly_natDegree`, `exists_isCartanSubalgebra_engel`, `exists_isCartanSubalgebra_engel_of_finrank_le_card`	7
Total	7

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`engel_isBot_of_isMin` 📖	mathematical	`LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Preorder.toLE` `PartialOrder.toPreorder` `LieSubalgebra.instPartialOrder_1` `Set` `Set.instMembership` `setOf` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.engel` `IsMin` `Set.Elem`	`IsBot`	—	`LieSubalgebra.lie_mem` `eq_or_ne` `LieSubalgebra.engel_zero` `LieSubmodule.instAddSubgroupClass` `LieSubmodule.instSMulMemClass` `LE.le.eq_or_lt` `Submodule.finrank_le` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `LieSubalgebra.toSubmodule_injective` `Submodule.eq_top_of_finrank_eq` `LieSubalgebra.instAddSubgroupClass` `LieSubmodule.instLieModule` `LieSubalgebra.lieModule` `lieAlgebraSelfModule` `Module.IsNoetherian.finite` `LieSubalgebra.instIsNoetherianSubtypeMem` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `Module.Free.of_divisionRing` `LieSubmodule.instIsNoetherianSubtypeMem` `LieSubmodule.Quotient.lieQuotientLieModule` `LieSubmodule.Quotient.isNoetherian` `Polynomial.eq_zero_of_forall_eval_zero_of_natDegree_lt_card` `instIsDomain` `Polynomial.coe_evalRingHom` `Polynomial.coeff_map` `smulCommClass_self` `IsScalarTower.left` `engel_isBot_of_isMin.lieCharpoly_map_eval` `Polynomial.constantCoeff_apply` `LinearMap.charpoly_constantCoeff_eq_zero_iff` `AddSubmonoidClass.toAddMemClass` `AddSubgroupClass.toAddSubmonoidClass` `AddSubmonoidClass.toZeroMemClass` `LieSubalgebra.self_mem_engel` `Subtype.coe_ne_coe` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass` `lie_self` `lt_of_lt_of_le` `Nat.cast_lt` `Cardinal.addLeftMono` `IsOrderedRing.toZeroLEOneClass` `Cardinal.isOrderedRing` `Cardinal.instCharZero` `lt_of_le_of_lt` `engel_isBot_of_isMin.lieCharpoly_coeff_natDegree` `zero_add` `zero_smul` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `LieSubmodule.Quotient.surjective_mk'` `LieSubmodule.Quotient.mk_eq_zero'` `pow_succ` `LE.le.trans` `Multiset.toFinset_card_le` `Polynomial.card_roots'` `Submodule.finrank_quotient_add_finrank` `IsDomain.hasRankNullity` `Cardinal.exists_finset_le_card` `le_trans` `Finset.le_card_sdiff` `Polynomial.eq_zero_of_natDegree_lt_card_of_eval_eq_zero'` `LinearMap.charpoly_eq_X_pow_iff` `LieSubmodule.Quotient.mk_eq_zero` `LieSubalgebra.mem_engel_iff` `LieModuleHom.instLinearMapClass` `pow_zero` `pow_succ'` `Module.End.mul_apply` `Nat.find_spec` `Mathlib.Tactic.Contrapose.contrapose₂` `Nat.find_min` `LE.le.ge` `LieSubmodule.coe_toEnd_pow` `Polynomial.coeff_X_pow` `LT.lt.ne` `LT.lt.le` `engel_isBot_of_isMin.lieCharpoly_natDegree` `Polynomial.Monic.eq_X_pow_iff_natDegree_le_natTrailingDegree` `engel_isBot_of_isMin.lieCharpoly_monic` `Polynomial.le_natTrailingDegree` `Polynomial.Monic.ne_zero` `Polynomial.nontrivial` `LinearMap.charpoly.congr_simp` `sub_add_cancel` `one_smul` `Polynomial.map_X` `Polynomial.map_pow`
`exists_isCartanSubalgebra_engel` 📖	mathematical	—	`LieSubalgebra.IsCartanSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra.engel`	—	`exists_isCartanSubalgebra_engel_of_finrank_le_card` `LE.le.trans` `Cardinal.natCast_le_aleph0` `Cardinal.infinite_iff`
`exists_isCartanSubalgebra_engel_of_finrank_le_card` 📖	mathematical	—	`LieSubalgebra.IsCartanSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LieSubalgebra.engel`	—	`Module.Free.of_divisionRing` `exists_isRegular_of_finrank_le_card` `instIsDomain` `LieSubalgebra.isNilpotent_of_forall_le_engel` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LieSubalgebra.self_mem_engel` `engel_isBot_of_isMin` `le_rfl` `IsScalarTower.left` `isRegular_iff_finrank_engel_eq_rank` `rank_le_finrank_engel` `LieSubalgebra.toSubmodule_injective` `Submodule.eq_of_le_of_finrank_le` `FiniteDimensional.finiteDimensional_submodule` `Eq.ge` `LieSubalgebra.normalizer_engel`

LieAlgebra.engel_isBot_of_isMin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`lieCharpoly_coeff_natDegree` 📖	mathematical	`Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	`Polynomial.natDegree` `Polynomial.coeff` `Polynomial` `Polynomial.semiring`	—	`mul_one` `Polynomial.coeff_map` `MvPolynomial.aeval_natDegree_le` `MvPolynomial.IsHomogeneous.totalDegree_le` `smulCommClass_self` `IsScalarTower.left` `LinearMap.polyCharpoly_coeff_isHomogeneous` `Polynomial.natDegree_add_le_of_degree_le` `LE.le.trans` `Polynomial.natDegree_C_mul_le` `Polynomial.natDegree_X` `Polynomial.natDegree_C` `Nat.instCanonicallyOrderedAdd`
`lieCharpoly_map_eval` 📖	mathematical	—	`Polynomial.map` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Polynomial.evalRingHom` `LinearMap.charpoly` `DFunLike.coe` `LieHom` `Module.End` `AddCommGroup.toAddCommMonoid` `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` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `LieRing.toAddCommGroup` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `LieAlgebra.toModule`	—	`smulCommClass_self` `IsScalarTower.left` `Polynomial.map_map` `RingHomInvPair.ids` `map_add` `SemilinearMapClass.toAddHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `mul_comm` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHomClass.toRingHom.congr_simp` `MvPolynomial.comp_aeval` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `LinearMap.charpoly.congr_simp` `LieHom.instLinearMapClass` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `Polynomial.aeval_C` `Polynomial.aeval_X` `LinearMap.polyCharpoly_map_eq_charpoly`
`lieCharpoly_monic` 📖	mathematical	—	`Polynomial.Monic` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring`	—	`Polynomial.Monic.map` `LinearMap.polyCharpoly_monic`
`lieCharpoly_natDegree` 📖	mathematical	—	`Polynomial.natDegree` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Polynomial.semiring` `Module.finrank` `AddCommGroup.toAddCommMonoid`	—	`Polynomial.Monic.natDegree_map` `Polynomial.nontrivial` `LinearMap.polyCharpoly_monic` `LinearMap.polyCharpoly_natDegree`

---

← Back to Index