Documentation Verification Report

Matrix

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

Statistics

Metric	Count
Definitions	0
Theorems `spectrum_toMatrix`, `spectrum_toMatrix'`, `iSup_eigenspace_toLin'_diagonal_eq_top`, `iSup_eigenspace_toLin_diagonal_eq_top`, `maxGenEigenspace_toLin'_diagonal_eq_eigenspace`, `maxGenEigenspace_toLin_diagonal_eq_eigenspace`, `spectrum_toLin`, `spectrum_toLin'`, `hasEigenvalue_toLin'_diagonal_iff`, `hasEigenvalue_toLin_diagonal_iff`, `hasEigenvector_toLin'_diagonal`, `hasEigenvector_toLin_diagonal`, `spectrum_diagonal`	13
Total	13

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`spectrum_toMatrix` 📖	mathematical	—	`spectrum` `Matrix` `CommRing.toCommSemiring` `Matrix.instRing` `CommRing.toRing` `Matrix.instAlgebra` `Ring.toSemiring` `Algebra.id` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Matrix.module` `Semiring.toModule` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix` `Finite.of_fintype` `Module.End.instRing` `Module.End.instAlgebra` `CommRing.toCommMonoid` `Algebra.toSMul` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`AlgEquiv.spectrum_eq` `smulCommClass_self` `IsScalarTower.left` `AlgEquiv.instAlgEquivClass`
`spectrum_toMatrix'` 📖	mathematical	—	`spectrum` `Matrix` `CommRing.toCommSemiring` `Matrix.instRing` `CommRing.toRing` `Matrix.instAlgebra` `Ring.toSemiring` `Algebra.id` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `LinearMap` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `addCommMonoid` `Matrix.addCommMonoid` `module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Matrix.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toMatrix'` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End.instRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `Module.End.instAlgebra` `Algebra.toSMul` `Pi.isScalarTower` `IsScalarTower.right`	—	`AlgEquiv.spectrum_eq` `Function.smulCommClass` `Algebra.to_smulCommClass` `Pi.isScalarTower` `IsScalarTower.right` `AlgEquiv.instAlgEquivClass`

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`iSup_eigenspace_toLin'_diagonal_eq_top` 📖	mathematical	—	`iSup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Pi.Function.module` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Module.End.eigenspace` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Matrix` `LinearMap` `Pi.addCommMonoid` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Top.top` `Submodule.instTop`	—	`iSup_eigenspace_toLin_diagonal_eq_top` `Finite.of_fintype`
`iSup_eigenspace_toLin_diagonal_eq_top` 📖	mathematical	—	`iSup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Module.End.eigenspace` `DFunLike.coe` `LinearEquiv` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Top.top` `Submodule.instTop`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Submodule.eq_top_iff_forall_basis_mem` `Submodule.mem_iSup_of_mem` `toLin_self` `Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_ite_eq'`
`maxGenEigenspace_toLin'_diagonal_eq_eigenspace` 📖	mathematical	—	`Module.End.maxGenEigenspace` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Pi.Function.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Matrix` `LinearMap` `Pi.addCommMonoid` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End.eigenspace`	—	`maxGenEigenspace_toLin_diagonal_eq_eigenspace` `Finite.of_fintype`
`maxGenEigenspace_toLin_diagonal_eq_eigenspace` 📖	mathematical	—	`Module.End.maxGenEigenspace` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `AddCommGroup.toAddCommMonoid` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.End.eigenspace`	—	`le_antisymm` `RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Module.End.mem_maxGenEigenspace` `Pi.sub_def` `diagonal_sub` `diagonal_smul` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `map_smul` `SemilinearMapClass.toMulActionSemiHomClass` `toLin_one` `mulVec_eq_sum` `Finset.sum_congr` `diagonal_transpose` `IsCentralScalar.op_smul_eq_smul` `Pi.isCentralScalar` `CommSemigroup.isCentralScalar` `Finset.sum_apply` `mul_one` `mul_ite` `MulZeroClass.mul_zero` `Finset.sum_ite_eq'` `IsDomain.to_noZeroDivisors` `isReduced_of_noZeroDivisors` `IsDomain.toNontrivial` `toLin_apply_eq_zero_iff` `diagonal_pow` `toLin_pow` `MulZeroClass.zero_mul` `zero_smul` `smul_zero` `mul_comm` `SemigroupAction.mul_smul` `toLin_apply` `Module.Basis.sum_repr` `Module.End.eigenspace_le_maxGenEigenspace`
`spectrum_toLin` 📖	mathematical	—	`spectrum` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `AddCommGroup.toAddCommMonoid` `Module.End.instRing` `Module.End.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` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `module` `Semiring.toModule` `LinearMap.module` `CommSemiring.toCommMonoid` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin` `Finite.of_fintype` `instRing` `instAlgebra`	—	`AlgEquiv.spectrum_eq` `smulCommClass_self` `IsScalarTower.left` `AlgEquiv.instAlgEquivClass`
`spectrum_toLin'` 📖	mathematical	—	`spectrum` `LinearMap` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `Pi.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Pi.Function.module` `Semiring.toModule` `Module.End.instRing` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Module.End.instAlgebra` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `Algebra.toSMul` `Pi.isScalarTower` `IsScalarTower.right` `DFunLike.coe` `LinearEquiv` `RingHomInvPair.ids` `Matrix` `addCommMonoid` `LinearMap.addCommMonoid` `module` `LinearMap.module` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `toLin'` `instRing` `instAlgebra` `Ring.toSemiring`	—	`AlgEquiv.spectrum_eq` `Function.smulCommClass` `Algebra.to_smulCommClass` `Pi.isScalarTower` `IsScalarTower.right` `AlgEquiv.instAlgEquivClass`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hasEigenvalue_toLin'_diagonal_iff` 📖	mathematical	—	`Module.End.HasEigenvalue` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Pi.Function.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Matrix` `LinearMap` `Pi.addCommMonoid` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`hasEigenvalue_toLin_diagonal_iff` `Pi.instModuleIsTorsionFree` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `NoZeroDivisors.toNoZeroSMulDivisors` `IsDomain.to_noZeroDivisors` `Finite.of_fintype`
`hasEigenvalue_toLin_diagonal_iff` 📖	mathematical	—	`Module.End.HasEigenvalue` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `AddCommGroup.toAddCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Matrix.module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin` `Finite.of_fintype` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Module.End.hasEigenvalue_of_hasEigenvector` `hasEigenvector_toLin_diagonal` `Mathlib.Tactic.Contrapose.contrapose₁` `eq_top_iff` `Module.Basis.span_eq` `Submodule.span_le` `Submodule.mem_iSup_of_mem` `Module.End.mem_eigenspace_iff` `Module.End.HasEigenvector.apply_eq_smul` `iSupIndep.disjoint_biSup` `Module.End.eigenspaces_iSupIndep` `disjoint_top`
`hasEigenvector_toLin'_diagonal` 📖	mathematical	—	`Module.End.HasEigenvector` `Pi.addCommGroup` `Ring.toAddCommGroup` `CommRing.toRing` `Pi.Function.module` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `DFunLike.coe` `LinearEquiv` `RingHom.id` `RingHomInvPair.ids` `Matrix` `LinearMap` `Pi.addCommMonoid` `Matrix.addCommMonoid` `LinearMap.addCommMonoid` `Matrix.module` `LinearMap.module` `Function.smulCommClass` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MulAction.toSemigroupAction` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `Algebra.to_smulCommClass` `Algebra.id` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin'` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.Basis` `Module.Basis.instFunLike` `Pi.basisFun` `Finite.of_fintype`	—	`hasEigenvector_toLin_diagonal` `Finite.of_fintype`
`hasEigenvector_toLin_diagonal` 📖	mathematical	—	`Module.End.HasEigenvector` `DFunLike.coe` `LinearEquiv` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomInvPair.ids` `Matrix` `LinearMap` `AddCommGroup.toAddCommMonoid` `Matrix.addCommMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `LinearMap.addCommMonoid` `Matrix.module` `Semiring.toModule` `LinearMap.module` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `EquivLike.toFunLike` `DFinsupp.instEquivLikeLinearEquiv` `Matrix.toLin` `Finite.of_fintype` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.Basis` `Module.Basis.instFunLike`	—	`RingHomInvPair.ids` `smulCommClass_self` `Finite.of_fintype` `Module.End.mem_eigenspace_iff` `Matrix.toLin_self` `Finset.sum_congr` `ite_smul` `zero_smul` `Finset.sum_ite_eq'` `Module.Basis.ne_zero`
`spectrum_diagonal` 📖	mathematical	—	`spectrum` `Matrix` `Semifield.toCommSemiring` `Field.toSemifield` `Matrix.instRing` `DivisionRing.toRing` `Field.toDivisionRing` `Matrix.instAlgebra` `Ring.toSemiring` `Algebra.id` `Matrix.diagonal` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Set.range`	—	`Set.ext` `smulCommClass_self` `IsScalarTower.left` `Finite.of_fintype` `AlgEquiv.spectrum_eq` `AlgEquiv.instAlgEquivClass` `Module.End.hasEigenvalue_iff_mem_spectrum` `FiniteDimensional.finiteDimensional_pi'` `FiniteDimensional.finiteDimensional_self` `hasEigenvalue_toLin'_diagonal_iff` `EuclideanDomain.toNontrivial` `instIsDomain`

---

← Back to Index