Charpoly

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

Statistics

Metric	Count
Definitions	0
Theorems hasEigenvalue_iff_isRoot_charpoly, mem_spectrum_iff_isRoot_charpoly	2
Total	2

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
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

---

← Back to Index