Documentation Verification Report

Minpoly

📁 Source: Mathlib/LinearAlgebra/Eigenspace/Minpoly.lean

Statistics

Metric	Count
Definitions `instFintypeEigenvalues`	1
Theorems `finite_spectrum`, `instFiniteSpectrum`, `aeval_apply_of_hasEigenvector`, `eigenspace_aeval_polynomial_degree_1`, `finite_hasEigenvalue`, `finite_spectrum`, `hasEigenvalue_iff_isRoot`, `hasEigenvalue_of_isRoot`, `isRoot_of_hasEigenvalue`, `ker_aeval_ring_hom'_unit_polynomial`	10
Total	11

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite_spectrum` 📖	mathematical	—	`Set.Finite` `spectrum` `Matrix` `Semifield.toCommSemiring` `Field.toSemifield` `instRing` `DivisionRing.toRing` `Field.toDivisionRing` `instAlgebra` `Ring.toSemiring` `Algebra.id`	—	`smulCommClass_self` `IsScalarTower.left` `Finite.of_fintype` `AlgEquiv.spectrum_eq` `AlgEquiv.instAlgEquivClass` `Module.End.finite_spectrum` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.finiteDimensional_self`
`instFiniteSpectrum` 📖	mathematical	—	`Finite` `Set.Elem` `spectrum` `Matrix` `Semifield.toCommSemiring` `Field.toSemifield` `instRing` `DivisionRing.toRing` `Field.toDivisionRing` `instAlgebra` `Ring.toSemiring` `Algebra.id`	—	`Set.finite_coe_iff` `finite_spectrum`

Module.End

Definitions

Name	Category	Theorems
`instFintypeEigenvalues` 📖	CompOp	3 math math: `LinearMap.IsSymmetric.diagonalization_apply_self_apply`, `LinearMap.IsSymmetric.diagonalization_symm_apply`, `LinearMap.IsSymmetric.eigenvectorBasis_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`aeval_apply_of_hasEigenvector` 📖	mathematical	`HasEigenvector`	`DFunLike.coe` `Module.End` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `AlgHom` `Polynomial` `Polynomial.semiring` `instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `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` `SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `AddCommGroup.toAddGroup` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `Polynomial.eval`	—	`Polynomial.induction_on` `smulCommClass_self` `IsScalarTower.left` `Polynomial.aeval_C` `Polynomial.eval_C` `map_add` `SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.eval_add` `add_smul` `mul_comm` `pow_succ'` `mul_assoc` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `mul_apply` `Polynomial.aeval_X` `Polynomial.eval_mul` `Polynomial.eval_pow` `Polynomial.eval_X` `MulActionSemiHomClass.map_smulₛₗ` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `mem_eigenspace_iff` `smul_smul`
`eigenspace_aeval_polynomial_degree_1` 📖	mathematical	`Polynomial.degree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `WithBot` `WithBot.one` `Nat.instOne`	`eigenspace` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Polynomial.coeff` `Polynomial.leadingCoeff` `LinearMap.ker` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Module.End` `Polynomial.semiring` `instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `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`	—	`smulCommClass_self` `IsScalarTower.left` `eigenspace_div` `Polynomial.leadingCoeff_eq_zero_iff_deg_eq_bot` `WithBot.one_ne_bot` `Polynomial.C_mul'` `Polynomial.aeval_def` `neg_smul` `sub_neg_eq_add` `Polynomial.eval₂_add` `Polynomial.eval₂_smul` `Polynomial.eval₂_X` `Algebra.smul_mul_assoc` `one_mul` `Polynomial.eval₂_C` `Polynomial.eq_X_add_C_of_degree_eq_one`
`finite_hasEigenvalue` 📖	mathematical	—	`Set.Finite` `HasEigenvalue`	—	`smulCommClass_self` `IsScalarTower.left` `minpoly.ne_zero` `IsDomain.toNontrivial` `Algebra.IsIntegral.isIntegral` `isIntegral` `Set.ext` `hasEigenvalue_iff_isRoot` `Polynomial.mem_rootSet_of_ne` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `Polynomial.IsRoot.eq_1` `Polynomial.coe_aeval_eq_eval` `Polynomial.rootSet_finite`
`finite_spectrum` 📖	mathematical	—	`Set.Finite` `spectrum` `Module.End` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `Semifield.toCommSemiring` `instRing` `instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `Algebra.toSMul` `CommSemiring.toSemiring` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`smulCommClass_self` `IsScalarTower.left` `Set.ext` `hasEigenvalue_iff_mem_spectrum` `finite_hasEigenvalue` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors`
`hasEigenvalue_iff_isRoot` 📖	mathematical	—	`HasEigenvalue` `Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly` `Module.End` `AddCommGroup.toAddCommMonoid` `instRing` `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` `isRoot_of_hasEigenvalue` `hasEigenvalue_of_isRoot`
`hasEigenvalue_of_isRoot` 📖	mathematical	`Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly` `Module.End` `AddCommGroup.toAddCommMonoid` `instRing` `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`	`HasEigenvalue`	—	`smulCommClass_self` `IsScalarTower.left` `Polynomial.dvd_iff_isRoot` `minpoly.min` `Polynomial.Monic.of_mul_monic_left` `Polynomial.monic_X_sub_C` `minpoly.monic` `Algebra.IsIntegral.isIntegral` `isIntegral` `LinearMap.ext` `Nat.cast_one` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Polynomial.degree_eq_natDegree` `minpoly.ne_zero` `IsDomain.toNontrivial` `MulZeroClass.mul_zero` `Polynomial.degree_X_sub_C` `Polynomial.degree_mul` `IsDomain.to_noZeroDivisors` `hasEigenvalue_of_hasEigenvector` `hasEigenvector_iff` `map_mul` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Polynomial.aeval_sub` `Polynomial.aeval_X` `Polynomial.aeval_C` `minpoly.aeval`
`isRoot_of_hasEigenvalue` 📖	mathematical	`HasEigenvalue`	`Polynomial.IsRoot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `minpoly` `Module.End` `AddCommGroup.toAddCommMonoid` `instRing` `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` `Submodule.ne_bot_iff` `smul_eq_zero` `IsDomain.toIsCancelMulZero` `aeval_apply_of_hasEigenvector` `minpoly.aeval`
`ker_aeval_ring_hom'_unit_polynomial` 📖	mathematical	—	`LinearMap.ker` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `DFunLike.coe` `AlgHom` `Polynomial` `Module.End` `Polynomial.semiring` `instSemiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `instAlgebra` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.funLike` `Polynomial.aeval` `Units.val` `Bot.bot` `Submodule` `Submodule.instBot`	—	`smulCommClass_self` `IsScalarTower.left` `LinearMap.ker_eq_bot'` `Units.inv_mul` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass`

---

← Back to Index