Eigs

📁 Source: Mathlib/LinearAlgebra/Matrix/Charpoly/Eigs.lean

Statistics

Metric	Count
Definitions	0
Theorems det_eq_prod_roots_charpoly, det_eq_prod_roots_charpoly_of_splits, mem_spectrum_iff_isRoot_charpoly, mem_spectrum_of_isRoot_charpoly, trace_eq_sum_roots_charpoly, trace_eq_sum_roots_charpoly_of_splits	6
Total	6

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
det_eq_prod_roots_charpoly 📖	mathematical	—	det EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.prod CommRing.toCommMonoid Polynomial.roots instIsDomain Field.toSemifield charpoly	—	det_eq_prod_roots_charpoly_of_splits IsAlgClosed.splits
det_eq_prod_roots_charpoly_of_splits 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain charpoly	det Multiset.prod CommRing.toCommMonoid Polynomial.roots instIsDomain Field.toSemifield	—	instIsDomain det_eq_sign_charpoly_coeff charpoly_natDegree_eq_dim IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.Splits.coeff_zero_eq_prod_roots_of_monic charpoly_monic mul_assoc pow_two pow_right_comm neg_one_sq one_pow one_mul
mem_spectrum_iff_isRoot_charpoly 📖	mathematical	—	Set Set.instMembership spectrum Matrix Semifield.toCommSemiring Field.toSemifield instRing DivisionRing.toRing Field.toDivisionRing instAlgebra Ring.toSemiring Algebra.id Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain charpoly	—	eval_charpoly
mem_spectrum_of_isRoot_charpoly 📖	mathematical	Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring charpoly	Set Set.instMembership spectrum Matrix instRing CommRing.toRing instAlgebra Ring.toSemiring Algebra.id	—	eval_charpoly NeZero.one
trace_eq_sum_roots_charpoly 📖	mathematical	—	trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Multiset.sum Polynomial.roots instIsDomain Field.toSemifield charpoly	—	trace_eq_sum_roots_charpoly_of_splits IsAlgClosed.splits
trace_eq_sum_roots_charpoly_of_splits 📖	mathematical	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain charpoly	trace NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Multiset.sum Polynomial.roots instIsDomain Field.toSemifield	—	instIsDomain isEmpty_or_nonempty trace.eq_1 Fintype.sum_empty charpoly.eq_1 det_eq_one_of_card_eq_zero Fintype.card_eq_zero_iff Polynomial.roots_one Multiset.empty_eq_zero Multiset.sum_zero trace_eq_neg_charpoly_nextCoeff neg_eq_iff_eq_neg Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic charpoly_monic

---

← Back to Index