Documentation Verification Report

Basic

📁 Source: Mathlib/LinearAlgebra/Charpoly/Basic.lean

Statistics

Metric	Count
Definitions `charpoly`	1
Theorems `aeval_eq_aeval_mod_charpoly`, `aeval_self_charpoly`, `charpoly_def`, `charpoly_monic`, `charpoly_natDegree`, `charpoly_one`, `charpoly_sub_smul`, `charpoly_zero`, `eval_charpoly`, `isIntegral`, `minpoly_coeff_zero_of_injective`, `minpoly_dvd_charpoly`, `pow_eq_aeval_mod_charpoly`	13
Total	14

LinearMap

Definitions

Name	Category	Theorems
`charpoly` 📖	CompOp	48 math math: `charpoly_def`, `isNilRegular_iff_natTrailingDegree_charpoly_eq_nilRank`, `LieAlgebra.finrank_engel`, `LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `charpoly_nilpotent_tfae`, `LieAlgebra.rank_le_natTrailingDegree_charpoly_ad`, `polyCharpolyAux_map_eval`, `Module.End.hasEigenvalue_iff_isRoot_charpoly`, `LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval`, `finrank_genEigenspace_le`, `IsNilpotent.charpoly_eq_X_pow_finrank`, `charpoly_monic`, `pow_eq_aeval_mod_charpoly`, `charpoly_eq_X_pow_iff`, `minpoly_dvd_charpoly`, `Matrix.charpoly_toLin`, `polyCharpolyAux_map_eq_charpoly`, `Matrix.charpoly_toLin'`, `aeval_eq_aeval_mod_charpoly`, `hasEigenvalue_zero_tfae`, `eval_charpoly`, `charpoly_constantCoeff_eq_zero_iff`, `Matrix.charpoly_mulVecLin`, `isNilpotent_iff_charpoly`, `det_eq_sign_charpoly_coeff`, `aeval_self_charpoly`, `LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank`, `polyCharpolyAux_map_aeval`, `finrank_maxGenEigenspace`, `polyCharpolyAux_coeff_eval`, `isNilpotent_tensor_residueField_iff`, `charpoly_one`, `polyCharpoly_map_eq_charpoly`, `charpoly_prodMap`, `charpoly_sub_smul`, `charpoly_natDegree`, `LinearEquiv.charpoly_conj`, `finrank_maxGenEigenspace_zero_eq`, `charpoly_zero`, `Module.End.mem_spectrum_iff_isRoot_charpoly`, `nilRank_le_natTrailingDegree_charpoly`, `not_hasEigenvalue_zero_tfae`, `finrank_maxGenEigenspace_eq`, `finrank_eigenspace_le`, `charpoly_baseChange`, `polyCharpoly_coeff_eval`, `LieModule.rank_le_natTrailingDegree_charpoly_ad`, `charpoly_toMatrix`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_eq_aeval_mod_charpoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.modByMonic` `charpoly`	—	`smulCommClass_self` `IsScalarTower.left` `Polynomial.aeval_modByMonic_eq_self_of_root` `charpoly_monic` `aeval_self_charpoly`
`aeval_self_charpoly` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval` `charpoly` `instZero`	—	`RingHomInvPair.ids` `smulCommClass_self` `IsScalarTower.left` `LinearEquiv.map_eq_zero_iff` `AlgEquiv.toLinearEquiv_apply` `AlgEquiv.coe_algHom` `Polynomial.aeval_algHom_apply` `AlgHom.algHomClass` `Finite.of_fintype` `charpoly_def` `Matrix.aeval_self_charpoly`
`charpoly_def` 📖	mathematical	—	`charpoly` `Matrix.charpoly` `Module.Free.ChooseBasisIndex` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Module.Free.instDecidableEqChooseBasisIndex` `Module.Free.ChooseBasisIndex.fintype` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Matrix` `addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype` `Module.Free.chooseBasis`	—	—
`charpoly_monic` 📖	mathematical	—	`Polynomial.Monic` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly`	—	`Matrix.charpoly_monic`
`charpoly_natDegree` 📖	mathematical	—	`Polynomial.natDegree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `Module.finrank` `AddCommGroup.toAddCommMonoid`	—	`charpoly.eq_1` `Matrix.charpoly_natDegree_eq_dim` `Module.finrank_eq_card_chooseBasisIndex`
`charpoly_one` 📖	mathematical	—	`charpoly` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instOne` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.instSub` `CommRing.toRing` `Polynomial.X` `Polynomial.instOne` `Module.finrank`	—	`Matrix.charpoly.congr_simp` `toMatrix_one` `Matrix.charpoly_one` `Module.finrank_eq_card_chooseBasisIndex`
`charpoly_sub_smul` 📖	mathematical	—	`charpoly` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `instSub` `RingHom.id` `Semiring.toNonAssocSemiring` `instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Ring.toSemiring` `CommRing.toRing` `Module.End.instOne` `Polynomial.comp` `Polynomial` `Polynomial.instAdd` `Polynomial.X` `DFunLike.coe` `RingHom` `Polynomial.semiring` `RingHom.instFunLike` `Polynomial.C`	—	`smulCommClass_self` `Matrix.charpoly.congr_simp` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `toMatrix_one` `Matrix.smul_eq_mul_diagonal` `one_mul` `Matrix.charpoly_sub_scalar`
`charpoly_zero` 📖	mathematical	—	`charpoly` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instZero` `Polynomial` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Module.finrank`	—	`Matrix.charpoly.congr_simp` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Matrix.charpoly_zero` `Module.finrank_eq_card_chooseBasisIndex`
`eval_charpoly` 📖	mathematical	—	`Polynomial.eval` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `charpoly` `DFunLike.coe` `MonoidHom` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Module.End.instSemiring` `MonoidHom.instFunLike` `det` `instSub` `RingHom` `RingHom.instFunLike` `algebraMap` `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`	—	`smulCommClass_self` `IsScalarTower.left` `charpoly.eq_1` `Matrix.eval_charpoly` `RingHomInvPair.ids` `Finite.of_fintype` `det_toMatrix` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Matrix.scalar_apply` `toMatrix_algebraMap`
`isIntegral` 📖	mathematical	—	`IsIntegral` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `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`	—	`smulCommClass_self` `IsScalarTower.left` `charpoly_monic` `aeval_self_charpoly`
`minpoly_coeff_zero_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `instFunLike`	—	—	`smulCommClass_self` `IsScalarTower.left` `Polynomial.X_dvd_iff` `mul_comm` `Polynomial.degree_lt_degree_mul_X` `minpoly.ne_zero` `isIntegral` `MulZeroClass.mul_zero` `minpoly.monic` `Polynomial.Monic.def` `Polynomial.leadingCoeff_mul_X` `minpoly.aeval` `not_le` `minpoly.min` `ext` `RingHomCompTriple.ids` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass`
`minpoly_dvd_charpoly` 📖	mathematical	—	`Polynomial` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `semigroupDvd` `SemigroupWithZero.toSemigroup` `NonUnitalSemiring.toSemigroupWithZero` `NonUnitalCommSemiring.toNonUnitalSemiring` `NonUnitalCommRing.toNonUnitalCommSemiring` `CommRing.toNonUnitalCommRing` `Polynomial.commRing` `minpoly` `LinearMap` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instRing` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `Semifield.toCommSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `charpoly` `Module.Free.of_divisionRing` `Field.toDivisionRing`	—	`minpoly.dvd` `smulCommClass_self` `IsScalarTower.left` `Module.Free.of_divisionRing` `aeval_self_charpoly`
`pow_eq_aeval_mod_charpoly` 📖	mathematical	—	`LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Monoid.toNatPow` `Module.End.instMonoid` `DFunLike.coe` `AlgHom` `Polynomial` `Polynomial.semiring` `Module.End.instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval` `Polynomial.modByMonic` `Polynomial.X` `charpoly`	—	`smulCommClass_self` `IsScalarTower.left` `aeval_eq_aeval_mod_charpoly` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X`

---

← Back to Index