Charpoly

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

Statistics

Metric	Count
Definitions	0
Theorems det_eq_prod_roots_charpoly_of_splits, hasEigenvalue_iff_isRoot_charpoly, mem_spectrum_iff_isRoot_charpoly, trace_eq_sum_roots_charpoly_of_splits	4
Total	4

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_eq_prod_roots_charpoly_of_splits 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain LinearMap.charpoly Module.Free.of_divisionRing Field.toDivisionRing	DFunLike.coe MonoidHom LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass instSemiring MonoidHom.instFunLike LinearMap.det Multiset.prod CommRing.toCommMonoid Polynomial.roots instIsDomain Field.toSemifield LinearMap.charpoly Module.Free.of_divisionRing Field.toDivisionRing	—	Module.Free.of_divisionRing instIsDomain RingHomInvPair.ids smulCommClass_self Finite.of_fintype LinearMap.det_toMatrix Matrix.det_eq_prod_roots_charpoly_of_splits LinearMap.charpoly_toMatrix
hasEigenvalue_iff_isRoot_charpoly 📖	mathematical	—	HasEigenvalue Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring LinearMap.charpoly	—	hasEigenvalue_iff smulCommClass_self eigenspace_def LinearMap.det_eq_zero_iff_ker_ne_bot LinearMap.det_eq_sign_charpoly_coeff LinearMap.charpoly_sub_smul Polynomial.coeff_zero_eq_eval_zero Polynomial.eval_comp Polynomial.eval_add Polynomial.eval_X Polynomial.eval_C zero_add IsDomain.to_noZeroDivisors isReduced_of_noZeroDivisors IsDomain.toNontrivial NeZero.one
mem_spectrum_iff_isRoot_charpoly 📖	mathematical	—	Set Set.instMembership 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 Polynomial.IsRoot CommRing.toCommSemiring LinearMap.charpoly Module.Free.of_divisionRing Field.toDivisionRing	—	smulCommClass_self IsScalarTower.left Module.Free.of_divisionRing hasEigenvalue_iff_mem_spectrum hasEigenvalue_iff_isRoot_charpoly instIsDomain
trace_eq_sum_roots_charpoly_of_splits 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain LinearMap.charpoly Module.Free.of_divisionRing Field.toDivisionRing	DFunLike.coe LinearMap CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Semiring.toModule LinearMap.instFunLike LinearMap.trace Multiset.sum NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.roots instIsDomain LinearMap.charpoly Module.Free.of_divisionRing Field.toDivisionRing	—	Module.Free.of_divisionRing smulCommClass_self instIsDomain RingHomInvPair.ids Finite.of_fintype LinearMap.trace_eq_matrix_trace Matrix.trace_eq_sum_roots_charpoly_of_splits LinearMap.charpoly_toMatrix

---

← Back to Index