Spectrum

📁 Source: Mathlib/Analysis/Matrix/Spectrum.lean

Statistics

Metric	Count
Definitions eigenvalues, eigenvalues₀, eigenvectorBasis, eigenvectorUnitary	4
Theorems charpoly_eq, conjStarAlgAut_star_eigenvectorUnitary, det_eq_prod_eigenvalues, eigenvalues_eq, eigenvalues_eq_eigenvalues_iff, eigenvalues_eq_zero_iff, eigenvalues_mem_spectrum_real, eigenvalues₀_antitone, eigenvectorUnitary_apply, eigenvectorUnitary_coe, eigenvectorUnitary_col_eq, eigenvectorUnitary_mulVec, eigenvectorUnitary_transpose_apply, exists_eigenvector_of_ne_zero, mulVec_eigenvectorBasis, rank_eq_card_non_zero_eigs, rank_eq_rank_diagonal, roots_charpoly_eq_eigenvalues, roots_charpoly_eq_eigenvalues₀, sort_roots_charpoly_eq_eigenvalues₀, spectral_theorem, spectrum_eq_image_range, spectrum_real_eq_range_eigenvalues, splits_charpoly, star_eigenvectorUnitary_mulVec, star_mul_self_mul_eq_diagonal, trace_eq_sum_eigenvalues, finite_real_spectrum, instFiniteElemRealSpectrum, spectrum_toEuclideanLin, spectrum_toLpLin	31
Total	35

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_real_spectrum 📖	mathematical	—	Set.Finite Real spectrum Matrix Real.instCommSemiring instRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra	—	spectrum.preimage_algebraMap isScalarTower IsScalarTower.right Set.Finite.preimage Function.Injective.injOn FaithfulSMul.algebraMap_injective Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing finite_spectrum
instFiniteElemRealSpectrum 📖	mathematical	—	Finite Set.Elem Real spectrum Matrix Real.instCommSemiring instRing NormedRing.toRing NormedCommRing.toNormedRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra	—	finite_real_spectrum
spectrum_toEuclideanLin 📖	mathematical	—	spectrum LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring EuclideanSpace ESeminormedAddCommMonoid.toAddCommMonoid PiLp.topologicalSpace ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing NormedCommRing.toNonUnitalNormedCommRing AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup NormedAddCommGroup.toAddCommGroup WithLp.instModule SeminormedAddCommGroup.toAddCommGroup Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring NormedRing.toRing NormedCommRing.toNormedRing NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace Semifield.toCommSemiring Module.End.instRing Module.End.instAlgebra CommSemiring.toSemiring WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction Function.smulCommClass AddCommMonoid.toAddMonoid Algebra.to_smulCommClass Algebra.id Algebra.toSMul WithLp.instIsScalarTower Pi.isScalarTower IsScalarTower.right DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid LinearMap.addCommMonoid module LinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toEuclideanLin instRing instAlgebra	—	spectrum_toLpLin Nat.instAtLeastTwoHAddOfNat
spectrum_toLpLin 📖	mathematical	—	spectrum LinearMap CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField DenselyNormedField.toNormedField RCLike.toDenselyNormedField RingHom.id Semiring.toNonAssocSemiring WithLp AddCommGroup.toAddCommMonoid WithLp.instAddCommGroup Pi.addCommGroup Ring.toAddCommGroup CommRing.toRing WithLp.instModule Pi.Function.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring Semiring.toModule Semifield.toCommSemiring Field.toSemifield Module.End.instRing Module.End.instAlgebra NormedSpace.toModule NonUnitalSeminormedRing.toSeminormedAddCommGroup NonUnitalSeminormedCommRing.toNonUnitalSeminormedRing SeminormedCommRing.toNonUnitalSeminormedCommRing NormedCommRing.toSeminormedCommRing NormedField.toNormedCommRing InnerProductSpace.toNormedSpace RCLike.innerProductSpace WithLp.instSMulCommClass SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulAction.toSemigroupAction DistribMulAction.toMulAction SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Module.toDistribMulAction Function.smulCommClass AddCommMonoid.toAddMonoid Algebra.to_smulCommClass Algebra.id Algebra.toSMul WithLp.instIsScalarTower Pi.isScalarTower IsScalarTower.right DivisionSemiring.toSemiring Semifield.toDivisionSemiring DFunLike.coe LinearEquiv RingHomInvPair.ids Matrix addCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing LinearMap.addCommMonoid module LinearMap.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv toLpLin instRing NormedRing.toRing NormedCommRing.toNormedRing instAlgebra	—	AlgEquiv.spectrum_eq smulCommClass_self IsScalarTower.left AlgEquiv.instAlgEquivClass Finite.of_fintype

Matrix.IsHermitian

Definitions

Name	Category	Theorems
eigenvalues 📖	CompOp	24 math math: eigenvalues_eq, Matrix.PosDef.eigenvalues_pos, rank_eq_rank_diagonal, eigenvalues_eq_eigenvalues_iff, charpoly_cfc_eq, Matrix.eigenvalues_conjTranspose_mul_self_nonneg, trace_eq_sum_eigenvalues, Matrix.PosSemidef.eigenvalues_nonneg, posSemidef_iff_eigenvalues_nonneg, Matrix.eigenvalues_self_mul_conjTranspose_nonneg, roots_charpoly_eq_eigenvalues, cfcAux_apply, det_eq_prod_eigenvalues, spectrum_eq_image_range, spectral_theorem, spectrum_real_eq_range_eigenvalues, eigenvalues_mem_spectrum_real, star_mul_self_mul_eq_diagonal, posDef_iff_eigenvalues_pos, eigenvalues_eq_zero_iff, rank_eq_card_non_zero_eigs, charpoly_eq, conjStarAlgAut_star_eigenvectorUnitary, mulVec_eigenvectorBasis
eigenvalues₀ 📖	CompOp	3 math math: eigenvalues₀_antitone, sort_roots_charpoly_eq_eigenvalues₀, roots_charpoly_eq_eigenvalues₀
eigenvectorBasis 📖	CompOp	8 math math: eigenvalues_eq, eigenvectorUnitary_col_eq, eigenvectorUnitary_mulVec, eigenvectorUnitary_apply, eigenvectorUnitary_coe, eigenvectorUnitary_transpose_apply, mulVec_eigenvectorBasis, star_eigenvectorUnitary_mulVec
eigenvectorUnitary 📖	CompOp	10 math math: eigenvectorUnitary_col_eq, eigenvectorUnitary_mulVec, cfcAux_apply, eigenvectorUnitary_apply, spectral_theorem, eigenvectorUnitary_coe, star_mul_self_mul_eq_diagonal, eigenvectorUnitary_transpose_apply, conjStarAlgAut_star_eigenvectorUnitary, star_eigenvectorUnitary_mulVec

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_eq 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Finset.prod Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing Finset.univ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub NormedRing.toRing NormedCommRing.toNormedRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C RCLike.ofReal eigenvalues	—	IsScalarTower.right Algebra.to_smulCommClass spectral_theorem Unitary.conjStarAlgAut_apply Matrix.charpoly_mul_comm mul_assoc Matrix.charpoly.congr_simp Unitary.star_mul_self_of_mem one_mul Matrix.charpoly_diagonal Finset.prod_congr
conjStarAlgAut_star_eigenvectorUnitary 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	DFunLike.coe StarAlgEquiv Matrix Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id StarMul.toInvolutiveStar StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing StarAlgEquiv.instFunLike MonoidHom Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike unitary MulOneClass.toMulOne Submonoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid StarAlgEquiv.aut MonoidHom.instFunLike Unitary.conjStarAlgAut IsScalarTower.right Matrix.instAlgebra Algebra.to_smulCommClass Star.star Unitary.instStarSubtypeMemSubmonoidUnitary eigenvectorUnitary Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real RCLike.ofReal eigenvalues	—	LinearEquiv.injective fact_one_le_two_ennreal WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass RingHomInvPair.ids IsScalarTower.right Module.Basis.ext Unitary.conjStarAlgAut_star_apply EuclideanSpace.basisFun_apply eigenvectorUnitary_mulVec mulVec_eigenvectorBasis RCLike.real_smul_eq_coe_smul Pi.isScalarTower Matrix.mulVec_smul star_eigenvectorUnitary_mulVec Matrix.diagonal_mulVec_single mul_one PiLp.ext EuclideanSpace.single_apply mul_ite MulZeroClass.mul_zero
det_eq_prod_eigenvalues 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.det EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Finset.prod CommRing.toCommMonoid Finset.univ RCLike.ofReal eigenvalues	—	instIsDomain Matrix.det_eq_prod_roots_charpoly_of_splits splits_charpoly roots_charpoly_eq_eigenvalues Multiset.map_congr
eigenvalues_eq 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	eigenvalues DFunLike.coe AddMonoidHom Real AddMonoid.toZero NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re dotProduct Distrib.toMul NonUnitalNonAssocSemiring.toDistrib ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Star.star Pi.instStarForall WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis Matrix.mulVec	—	fact_one_le_two_ennreal dotProduct_comm mulVec_eigenvectorBasis smul_dotProduct IsScalarTower.right Nat.instAtLeastTwoHAddOfNat inner_self_eq_norm_sq_to_K OrthonormalBasis.orthonormal algebraMap.coe_one one_pow RCLike.smul_re RCLike.one_re mul_one
eigenvalues_eq_eigenvalues_iff 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	eigenvalues Matrix.charpoly EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField	—	charpoly_eq instIsDomain instIsTransGe instAntisymmGe LE.total' Multiset.sort.congr_simp Multiset.map_congr Polynomial.roots.congr_simp
eigenvalues_eq_zero_iff 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	eigenvalues Pi.instZero Real Real.instZero Matrix Matrix.zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	IsScalarTower.right Algebra.to_smulCommClass spectral_theorem Pi.comp_zero RCLike.ofReal_zero Function.const_zero Pi.zero_def Matrix.diagonal_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass fact_one_le_two_ennreal eigenvalues.congr_simp eigenvalues_eq Matrix.zero_mulVec dotProduct_zero AddMonoidHomClass.toZeroHomClass AddMonoidHom.instAddMonoidHomClass
eigenvalues_mem_spectrum_real 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Real Set Set.instMembership spectrum Matrix Real.instCommSemiring Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra eigenvalues	—	spectrum.of_algebraMap_mem Matrix.isScalarTower IsScalarTower.right Nat.instAtLeastTwoHAddOfNat WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass WithLp.instIsScalarTower Pi.isScalarTower RingHomInvPair.ids Matrix.spectrum_toLpLin Module.End.HasEigenvalue.mem_spectrum fact_one_le_two_ennreal finrank_euclideanSpace LinearMap.IsSymmetric.hasEigenvalue_eigenvalues
eigenvalues₀_antitone 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Antitone Fintype.card Real PartialOrder.toPreorder Fin.instPartialOrder Real.instPreorder eigenvalues₀	—	LinearMap.IsSymmetric.eigenvalues_antitone fact_one_le_two_ennreal finrank_euclideanSpace
eigenvectorUnitary_apply 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis	—	—
eigenvectorUnitary_coe 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary Module.Basis.toMatrix EuclideanSpace Semifield.toCommSemiring Field.toSemifield ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedAddCommGroup.toPseudoMetricSpace NormedAddCommGroup.toSeminormedAddCommGroup PiLp.normedAddCommGroup ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NormedSpace.toModule InnerProductSpace.toNormedSpace PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.toBasis EuclideanSpace.basisFun DFunLike.coe Module.Basis DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.Basis.instFunLike eigenvectorBasis	—	—
eigenvectorUnitary_col_eq 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.col Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis	—	—
eigenvectorUnitary_mulVec 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.mulVec Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis	—	fact_one_le_two_ennreal Matrix.mulVec_single_one
eigenvectorUnitary_transpose_apply 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.transpose Matrix Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis	—	—
exists_eigenvector_of_ne_zero 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.mulVec Real Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra	—	Mathlib.Tactic.Contrapose.contrapose₄ IsScalarTower.right Algebra.to_smulCommClass spectral_theorem map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass instAlgEquivClassOfNonUnitalAlgEquivClass StarAlgEquiv.instNonUnitalAlgEquivClass Matrix.diagonal_zero RCLike.ofReal_zero Pi.comp_zero Function.ne_iff Nat.instAtLeastTwoHAddOfNat fact_one_le_two_ennreal Iff.ne WithLp.ofLp_eq_zero Orthonormal.ne_zero OrthonormalBasis.orthonormal mulVec_eigenvectorBasis
mulVec_eigenvectorBasis 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.mulVec WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis Real Function.hasSMul Algebra.toSMul Semifield.toCommSemiring Field.toSemifield NormedField.toField Real.normedField Ring.toSemiring SeminormedRing.toRing SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing NormedAlgebra.toAlgebra RCLike.toNormedAlgebra eigenvalues	—	fact_one_le_two_ennreal finrank_euclideanSpace OrthonormalBasis.reindex_apply RCLike.real_smul_eq_coe_smul Pi.isScalarTower IsScalarTower.right RingHomInvPair.ids WithLp.instSMulCommClass Function.smulCommClass Algebra.to_smulCommClass WithLp.instModuleFinite FiniteDimensional.finiteDimensional_pi' Finite.of_fintype Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self Matrix.isHermitian_iff_isSymmetric Fintype.card_fin LinearMap.IsSymmetric.apply_eigenvectorBasis
rank_eq_card_non_zero_eigs 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.rank EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Fintype.card Real eigenvalues Real.instZero Subtype.fintype Real.decidableEq	—	rank_eq_rank_diagonal Matrix.rank_diagonal
rank_eq_rank_diagonal 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.rank EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Real Real.commRing Matrix.diagonal Real.instZero eigenvalues	—	IsScalarTower.right Algebra.to_smulCommClass spectral_theorem Unitary.conjStarAlgAut_apply Unitary.coe_star Matrix.rank_mul_eq_left_of_isUnit_det Matrix.rank_mul_eq_right_of_isUnit_det Matrix.rank_diagonal Fintype.card_congr' IsLocalRing.toNontrivial Field.instIsLocalRing RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Fintype.card_subtype_compl
roots_charpoly_eq_eigenvalues 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instIsDomain Field.toSemifield Matrix.charpoly Multiset.map Real RCLike.ofReal eigenvalues Finset.val Finset.univ	—	instIsDomain charpoly_eq Polynomial.roots_prod Polynomial.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.instNoZeroDivisors NormMulClass.toNoZeroDivisors NormedDivisionRing.toNormMulClass Polynomial.roots_X_sub_C Multiset.bind_singleton Multiset.map_congr
roots_charpoly_eq_eigenvalues₀ 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField instIsDomain Field.toSemifield Matrix.charpoly Multiset.map Fintype.card Real RCLike.ofReal eigenvalues₀ Finset.val Finset.univ Fin.fintype	—	instIsDomain roots_charpoly_eq_eigenvalues Multiset.map_congr Multiset.map_univ_val_equiv Fin.univ_val_map List.map_ofFn
sort_roots_charpoly_eq_eigenvalues₀ 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Multiset.sort Real Multiset.map DFunLike.coe AddMonoidHom AddMonoid.toZero NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring Ring.toSemiring CommRing.toRing Field.toCommRing NormedField.toField AddSemigroup.toAdd AddMonoid.toAddSemigroup AddZeroClass.toAddZero AddMonoid.toAddZeroClass Real.instAddMonoid AddMonoidHom.instFunLike RCLike.re Polynomial.roots EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Matrix.charpoly Real.instLE Real.decidableLE instIsTransGe Real.instPreorder instAntisymmGe Real.partialOrder LE.total' Real.linearOrder Fintype.card eigenvalues₀	—	instIsDomain instIsTransGe instAntisymmGe LE.total' Multiset.sort.congr_simp Multiset.map_congr roots_charpoly_eq_eigenvalues₀ Fin.univ_val_map List.map_ofFn RCLike.ofReal_re Antitone.sortedGE_ofFn eigenvalues₀_antitone
spectral_theorem 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	DFunLike.coe StarAlgEquiv Matrix Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id StarMul.toInvolutiveStar StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing StarAlgEquiv.instFunLike MonoidHom Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike unitary MulOneClass.toMulOne Submonoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid StarAlgEquiv.aut MonoidHom.instFunLike Unitary.conjStarAlgAut IsScalarTower.right Matrix.instAlgebra Algebra.to_smulCommClass eigenvectorUnitary Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real RCLike.ofReal eigenvalues	—	IsScalarTower.right Algebra.to_smulCommClass conjStarAlgAut_star_eigenvectorUnitary Unitary.conjStarAlgAut_mul_apply Unitary.mul_star_self map_one MonoidHomClass.toOneHomClass MonoidHom.instMonoidHomClass
spectrum_eq_image_range 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	spectrum Matrix Semifield.toCommSemiring Field.toSemifield NormedField.toField Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring Algebra.id Set.image Real RCLike.ofReal Set.range eigenvalues	—	Set.ext IsScalarTower.right Algebra.to_smulCommClass spectral_theorem Unitary.spectrum_star_right_conjugate spectrum_diagonal
spectrum_real_eq_range_eigenvalues 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	spectrum Real Matrix Real.instCommSemiring Matrix.instRing NormedRing.toRing NormedCommRing.toNormedRing Matrix.instAlgebra Ring.toSemiring NormedAlgebra.toAlgebra Real.normedField SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing RCLike.toNormedAlgebra Set.range eigenvalues	—	Set.ext IsScalarTower.right Algebra.to_smulCommClass spectral_theorem spectrum.algebraMap_mem_iff Matrix.isScalarTower Unitary.spectrum_star_right_conjugate spectrum_diagonal Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing
splits_charpoly 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Polynomial.Splits CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField Matrix.charpoly	—	instIsDomain Polynomial.splits_iff_card_roots roots_charpoly_eq_eigenvalues Multiset.map_congr Multiset.card_map Matrix.charpoly_natDegree_eq_dim IsLocalRing.toNontrivial Field.instIsLocalRing
star_eigenvectorUnitary_mulVec 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.mulVec Star.star Matrix Matrix.instStar Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Matrix.nonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain NormedField.toField SetLike.instMembership Submonoid.instSetLike Matrix.unitaryGroup eigenvectorUnitary WithLp.ofLp ENNReal instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOneENNReal DFunLike.coe OrthonormalBasis EuclideanSpace PiLp.normedAddCommGroup fact_one_le_two_ennreal NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing PiLp.innerProductSpace RCLike.innerProductSpace OrthonormalBasis.instFunLike eigenvectorBasis Pi.single MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne NormedRing.toRing NormedCommRing.toNormedRing	—	fact_one_le_two_ennreal eigenvectorUnitary_mulVec Matrix.mulVec_mulVec Unitary.coe_star_mul_self Matrix.one_mulVec
star_mul_self_mul_eq_diagonal 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	DFunLike.coe StarAlgEquiv Matrix Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Matrix.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield NormedField.toField Distrib.toMul Matrix.smul Algebra.toSMul Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id StarMul.toInvolutiveStar StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Matrix.instStarRing NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing StarAlgEquiv.instFunLike MonoidHom Submonoid Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero SetLike.instMembership Submonoid.instSetLike unitary MulOneClass.toMulOne Submonoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid StarAlgEquiv.aut MonoidHom.instFunLike Unitary.conjStarAlgAut IsScalarTower.right Matrix.instAlgebra Algebra.to_smulCommClass Star.star Unitary.instStarSubtypeMemSubmonoidUnitary eigenvectorUnitary Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass Real RCLike.ofReal eigenvalues	—	conjStarAlgAut_star_eigenvectorUnitary
trace_eq_sum_eigenvalues 📖	mathematical	Matrix.IsHermitian InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing NonUnitalNormedCommRing.toNonUnitalCommRing NormedCommRing.toNonUnitalNormedCommRing NormedField.toNormedCommRing DenselyNormedField.toNormedField RCLike.toDenselyNormedField StarRing.toStarAddMonoid RCLike.toStarRing	Matrix.trace ESeminormedAddCommMonoid.toAddCommMonoid UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace SeminormedRing.toPseudoMetricSpace SeminormedCommRing.toSeminormedRing NormedCommRing.toSeminormedCommRing ENormedAddCommMonoid.toESeminormedAddCommMonoid NormedAddCommGroup.toENormedAddCommMonoid NonUnitalNormedRing.toNormedAddCommGroup NonUnitalNormedCommRing.toNonUnitalNormedRing Finset.sum Finset.univ RCLike.ofReal eigenvalues	—	instIsDomain Matrix.trace_eq_sum_roots_charpoly_of_splits splits_charpoly roots_charpoly_eq_eigenvalues Multiset.map_congr

---

← Back to Index