Documentation Verification Report

Basic

📁 Source: Mathlib/Algebra/Lie/AdjointAction/Basic.lean

Statistics

Metric	Count
Definitions	0
Theorems `ad_isSemisimple_of_isSemisimple`, `ad_nilpotent_of_nilpotent`, `commute_ad_of_commute`, `isNilpotent_ad_of_isNilpotent`, `isNilpotent_ad_of_isNilpotent_ad`	5
Total	5

LieAlgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ad_isSemisimple_of_isSemisimple` 📖	mathematical	—	`Module.End.IsSemisimple` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `LinearMap.addCommGroup` `RingHom.id` `Semiring.toNonAssocSemiring` `toModule` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `CommRing.toCommSemiring` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DFunLike.coe` `LieHom` `LieRing.toAddCommGroup` `LieHom.instFunLike` `ad`	—	`smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right` `ad_eq_lmul_left_sub_lmul_right` `Module.End.isSemisimple_of_squarefree_aeval_eq_zero` `Module.End.IsSemisimple.minpoly_squarefree` `LinearMap.instSMulCommClass` `LinearMap.instIsScalarTower` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `minpoly.aeval` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `IsScalarTower.to_smulCommClass'` `IsScalarTower.opposite_mid` `LinearMap.ext` `Polynomial.aeval_op_apply` `MulOpposite.op_zero` `Module.End.IsSemisimple.sub_of_commute` `Module.IsNoetherian.finite` `isNoetherian_linearMap` `isNoetherian_of_isNoetherianRing_of_finite` `IsSimpleModule.instIsNoetherian` `instIsSimpleModule` `LinearMap.commute_mulLeft_right`
`ad_nilpotent_of_nilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	`IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `toModule` `ofAssociativeAlgebra` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `Module.End.instMonoid` `DFunLike.coe` `LieHom` `Module.End.instRing` `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`	—	`smulCommClass_self` `IsScalarTower.left` `Algebra.to_smulCommClass` `IsScalarTower.right` `ad_eq_lmul_left_sub_lmul_right` `LinearMap.isNilpotent_mulLeft_iff` `LinearMap.isNilpotent_mulRight_iff` `Commute.isNilpotent_sub` `LinearMap.commute_mulLeft_right`
`commute_ad_of_commute` 📖	mathematical	`Commute` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing`	`Commute` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieRing.ofAssociativeRing` `toModule` `ofAssociativeAlgebra` `Module.End.instMul` `DFunLike.coe` `LieHom` `Module.End.instRing` `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`	—	`smulCommClass_self` `IsScalarTower.left` `Commute.eq_1` `SemiconjBy.eq_1` `sub_eq_zero` `Ring.lie_def` `LieHom.map_lie` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LieHom.instLinearMapClass`
`isNilpotent_ad_of_isNilpotent` 📖	mathematical	`IsNilpotent` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `LieSubalgebra` `LieRing.ofAssociativeRing` `ofAssociativeAlgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike`	`IsNilpotent` `Module.End` `LieSubalgebra` `LieRing.ofAssociativeRing` `ofAssociativeAlgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `toModule` `LieSubalgebra.lieAlgebra` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `Module.End.instMonoid` `DFunLike.coe` `LieHom` `Module.End.instRing` `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`	—	`LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad` `ad_nilpotent_of_nilpotent`

LieSubalgebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isNilpotent_ad_of_isNilpotent_ad` 📖	mathematical	`IsNilpotent` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `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` `LieAlgebra.ad` `LieSubalgebra` `SetLike.instMembership` `instSetLike`	`IsNilpotent` `Module.End` `LieSubalgebra` `SetLike.instMembership` `instSetLike` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `lieRing` `LieAlgebra.toModule` `lieAlgebra` `LinearMap.instZero` `RingHom.id` `Semiring.toNonAssocSemiring` `Monoid.toPow` `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` `LieAlgebra.ad`	—	`smulCommClass_self` `IsScalarTower.left` `Module.End.submodule_pow_eq_zero_of_pow_eq_zero` `ad_comp_incl_eq`

---

← Back to Index