Documentation Verification Report

Rank

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

Statistics

Metric	Count
Definitions `IsRegular`, `rank`, `IsRegular`, `rank`	4
Theorems `exists_isRegular`, `exists_isRegular_of_finrank_le_card`, `finrank_engel`, `isRegular_def`, `isRegular_iff_coeff_polyCharpoly_rank_ne_zero`, `isRegular_iff_finrank_engel_eq_rank`, `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `polyCharpoly_coeff_rank_ne_zero`, `rank_eq_natTrailingDegree`, `rank_le_card`, `rank_le_finrank`, `rank_le_finrank_engel`, `rank_le_natTrailingDegree_charpoly_ad`, `exists_isRegular`, `exists_isRegular_of_finrank_le_card`, `isRegular_def`, `isRegular_iff_coeff_polyCharpoly_rank_ne_zero`, `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `polyCharpoly_coeff_rank_ne_zero`, `rank_eq_natTrailingDegree`, `rank_le_card`, `rank_le_finrank`, `rank_le_natTrailingDegree_charpoly_ad`	23
Total	27

LieAlgebra

Definitions

Name	Category	Theorems
`IsRegular` 📖	MathDef	6 math math: `exists_isRegular`, `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `exists_isRegular_of_finrank_le_card`, `isRegular_iff_coeff_polyCharpoly_rank_ne_zero`, `isRegular_def`, `isRegular_iff_finrank_engel_eq_rank`
`rank` 📖	CompOp	7 math math: `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `rank_le_card`, `rank_le_natTrailingDegree_charpoly_ad`, `rank_le_finrank_engel`, `rank_le_finrank`, `rank_eq_natTrailingDegree`, `isRegular_iff_finrank_engel_eq_rank`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isRegular` 📖	mathematical	—	`IsRegular`	—	`LinearMap.exists_isNilRegular` `lieAlgebraSelfModule`
`exists_isRegular_of_finrank_le_card` 📖	mathematical	—	`IsRegular`	—	`LinearMap.exists_isNilRegular_of_finrank_le_card` `lieAlgebraSelfModule`
`finrank_engel` 📖	mathematical	—	`Module.finrank` `LieSubalgebra` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.engel` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `LieSubalgebra.lieRing` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `toModule` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Polynomial.natTrailingDegree` `CommRing.toCommSemiring` `LinearMap.charpoly` `Module.Free.of_divisionRing` `Field.toDivisionRing` `DFunLike.coe` `LieHom` `Module.End` `LieRing.ofAssociativeRing` `Module.End.instRing` `ofAssociativeAlgebra` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `LieHom.instFunLike` `ad`	—	`LinearMap.finrank_maxGenEigenspace_zero_eq` `smulCommClass_self` `IsScalarTower.left`
`isRegular_def` 📖	mathematical	—	`IsRegular`	—	—
`isRegular_iff_coeff_polyCharpoly_rank_ne_zero` 📖	mathematical	—	`IsRegular`	—	`LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero` `lieAlgebraSelfModule`
`isRegular_iff_finrank_engel_eq_rank` 📖	mathematical	—	`IsRegular` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.Free.of_divisionRing` `Field.toDivisionRing` `LieRing.toAddCommGroup` `toModule` `Module.finrank` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.engel` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.lieRing` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `rank`	—	`Module.Free.of_divisionRing` `IsScalarTower.left` `smulCommClass_self` `isRegular_iff_natTrailingDegree_charpoly_eq_rank` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `finrank_engel`
`isRegular_iff_natTrailingDegree_charpoly_eq_rank` 📖	mathematical	—	`IsRegular` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `LinearMap.charpoly` `LieRing.toAddCommGroup` `toModule` `DFunLike.coe` `LieHom` `Module.End` `AddCommGroup.toAddCommMonoid` `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` `rank`	—	`LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank` `lieAlgebraSelfModule`
`polyCharpoly_coeff_rank_ne_zero` 📖	—	—	—	—	`LinearMap.polyCharpoly_coeff_nilRank_ne_zero` `smulCommClass_self` `IsScalarTower.left`
`rank_eq_natTrailingDegree` 📖	mathematical	—	`rank` `Polynomial.natTrailingDegree` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `LinearMap.polyCharpoly` `LieRing.toAddCommGroup` `toModule` `LieHom.toLinearMap` `Module.End` `AddCommGroup.toAddCommMonoid` `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` `ad`	—	`LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree` `lieAlgebraSelfModule`
`rank_le_card` 📖	mathematical	—	`rank` `Fintype.card`	—	`LinearMap.nilRank_le_card` `lieAlgebraSelfModule`
`rank_le_finrank` 📖	mathematical	—	`rank` `Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LieRing.toAddCommGroup` `toModule`	—	`LinearMap.nilRank_le_finrank` `lieAlgebraSelfModule`
`rank_le_finrank_engel` 📖	mathematical	—	`rank` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Module.Free.of_divisionRing` `Field.toDivisionRing` `LieRing.toAddCommGroup` `toModule` `Module.finrank` `LieSubalgebra` `SetLike.instMembership` `LieSubalgebra.instSetLike` `LieSubalgebra.engel` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `LieSubalgebra.lieRing` `LieSubalgebra.instModuleSubtypeMemOfIsScalarTower` `Algebra.toSMul` `Semifield.toCommSemiring` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction`	—	`LE.le.trans` `Module.Free.of_divisionRing` `smulCommClass_self` `IsScalarTower.left` `rank_le_natTrailingDegree_charpoly_ad` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Eq.ge` `finrank_engel`
`rank_le_natTrailingDegree_charpoly_ad` 📖	mathematical	—	`rank` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `LinearMap.charpoly` `LieRing.toAddCommGroup` `toModule` `DFunLike.coe` `LieHom` `Module.End` `AddCommGroup.toAddCommMonoid` `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`	—	`LinearMap.nilRank_le_natTrailingDegree_charpoly` `lieAlgebraSelfModule`

LieModule

Definitions

Name	Category	Theorems
`IsRegular` 📖	MathDef	5 math math: `isRegular_iff_coeff_polyCharpoly_rank_ne_zero`, `exists_isRegular_of_finrank_le_card`, `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `isRegular_def`, `exists_isRegular`
`rank` 📖	CompOp	5 math math: `rank_le_finrank`, `rank_eq_natTrailingDegree`, `isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `rank_le_card`, `rank_le_natTrailingDegree_charpoly_ad`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_isRegular` 📖	mathematical	—	`IsRegular`	—	`LinearMap.exists_isNilRegular`
`exists_isRegular_of_finrank_le_card` 📖	mathematical	—	`IsRegular`	—	`LinearMap.exists_isNilRegular_of_finrank_le_card`
`isRegular_def` 📖	mathematical	—	`IsRegular`	—	—
`isRegular_iff_coeff_polyCharpoly_rank_ne_zero` 📖	mathematical	—	`IsRegular`	—	`LinearMap.isNilRegular_iff_coeff_polyCharpoly_nilRank_ne_zero`
`isRegular_iff_natTrailingDegree_charpoly_eq_rank` 📖	mathematical	—	`IsRegular` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `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` `toEnd` `rank`	—	`LinearMap.isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`
`polyCharpoly_coeff_rank_ne_zero` 📖	—	—	—	—	`LinearMap.polyCharpoly_coeff_nilRank_ne_zero` `smulCommClass_self` `IsScalarTower.left`
`rank_eq_natTrailingDegree` 📖	mathematical	—	`rank` `Polynomial.natTrailingDegree` `MvPolynomial` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `MvPolynomial.commSemiring` `LinearMap.polyCharpoly` `LieRing.toAddCommGroup` `LieAlgebra.toModule` `LieHom.toLinearMap` `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` `toEnd`	—	`LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree`
`rank_le_card` 📖	mathematical	—	`rank` `Fintype.card`	—	`LinearMap.nilRank_le_card`
`rank_le_finrank` 📖	mathematical	—	`rank` `Module.finrank` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid`	—	`LinearMap.nilRank_le_finrank`
`rank_le_natTrailingDegree_charpoly_ad` 📖	mathematical	—	`rank` `Polynomial.natTrailingDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `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` `toEnd`	—	`LinearMap.nilRank_le_natTrailingDegree_charpoly`

---

← Back to Index