Documentation Verification Report

Triangularizable

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

Statistics

Metric	Count
Definitions `instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial`	1
Theorems `exists_eigenvalue`, `exists_hasEigenvalue_of_genEigenspace_eq_top`, `genEigenspace_restrict_eq_top`, `iSup_maxGenEigenspace_eq_top`, `eq_iSup_inf_genEigenspace`, `inf_iSup_genEigenspace`	6
Total	7

Module.End

Definitions

Name	Category	Theorems
`instInhabitedEigenvaluesOfIsAlgClosedOfFiniteDimensionalOfNontrivial` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_eigenvalue` 📖	mathematical	—	`HasEigenvalue` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`smulCommClass_self` `IsScalarTower.left` `spectrum.nonempty_of_isAlgClosed_of_finiteDimensional` `instNontrivialLinearMapId` `Module.Finite.linearMap` `Module.Free.of_divisionRing`
`exists_hasEigenvalue_of_genEigenspace_eq_top` 📖	mathematical	`iSup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `DFunLike.coe` `OrderHom` `ENat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Submodule.instPartialOrder` `OrderHom.instFunLike` `genEigenspace` `Top.top` `Submodule.instTop`	`HasEigenvalue`	—	`Submodule.instNontrivial` `HasUnifEigenvalue.lt` `zero_lt_one` `IsOrderedRing.toZeroLEOneClass` `NeZero.charZero_one`
`genEigenspace_restrict_eq_top` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `iSup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `OrderHom` `ENat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `Submodule.instPartialOrder` `OrderHom.instFunLike` `genEigenspace` `Top.top` `Submodule.instTop`	`Submodule.addCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Submodule.module` `LinearMap.restrict`	—	`Submodule.eq_iSup_inf_genEigenspace` `Subtype.coe_injective` `RingHomSurjective.ids` `Submodule.comap_map_eq_of_injective` `Submodule.comap_subtype_self` `Submodule.inf_genEigenspace`
`iSup_maxGenEigenspace_eq_top` 📖	mathematical	—	`iSup` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AddCommGroup.toAddCommMonoid` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `maxGenEigenspace` `Top.top` `Submodule.instTop`	—	`Nat.strong_induction_on` `top_le_iff` `Submodule.finrank_eq_zero` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.Finite.top` `finrank_top` `exists_eigenvalue` `Module.finrank_pos_iff` `map_genEigenrange_le` `Submodule.mem_map_of_mem` `RingHomSurjective.ids` `pos_finrank_genEigenspace_of_hasEigenvalue` `smulCommClass_self` `genEigenspace_nat` `genEigenrange_nat` `LinearMap.finrank_range_add_finrank_ker` `FiniteDimensional.finiteDimensional_submodule` `Submodule.map_iSup` `Submodule.map.congr_simp` `Submodule.map_subtype_top` `maxGenEigenspace.eq_1` `genEigenspace_restrict` `Submodule.map_comap_le` `iSup_mono` `LE.le.trans` `OrderHom.mono` `le_top` `le_iSup` `generalized_eigenvec_disjoint_range_ker` `Submodule.eq_top_of_disjoint` `Eq.ge` `sup_le`

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_iSup_inf_genEigenspace` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring` `iSup` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `OrderHom` `ENat` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instPartialOrder` `OrderHom.instFunLike` `Module.End.genEigenspace` `Top.top` `instTop`	`instMin`	—	`inf_iSup_genEigenspace` `inf_top_eq`
`inf_iSup_genEigenspace` 📖	mathematical	`Submodule` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `setLike` `DFunLike.coe` `Module.End` `LinearMap.instFunLike` `RingHom.id` `Semiring.toNonAssocSemiring`	`instMin` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `OrderHom` `ENat` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrderENat` `instPartialOrder` `OrderHom.instFunLike` `Module.End.genEigenspace`	—	`le_antisymm` `mem_iSup_iff_exists_finsupp` `smulCommClass_self` `IsScalarTower.left` `Commute.pow_pow` `Commute.sub_left` `Commute.sub_right` `Algebra.commute_algebraMap_right` `Algebra.commute_algebraMap_left` `Finset.noncommProd_commute` `Commute.pow_right` `LinearMap.mem_ker` `Algebra.algebraMap_eq_smul_one` `Module.End.mem_genEigenspace_nat` `IsOrderedAddMonoid.toAddLeftMono` `LinearOrderedAddCommMonoidWithTop.toIsOrderedAddMonoid` `IsOrderedRing.toZeroLEOneClass` `Finset.le_sup` `OrderHom.mono` `Finset.mem_of_mem_erase` `Finset.noncommProd_erase_mul` `Finset.mem_erase` `Module.End.mul_apply` `map_zero` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `LinearMap.semilinearMapClass` `map_finsuppSum` `Finsupp.sum_congr` `Finsupp.sum_ite_eq'` `Finset.noncommProd_induction` `Set.MapsTo.comp` `Set.mapsTo_id` `LinearMap.sub_apply` `Module.algebraMap_end_apply` `sub_mem` `smul_mem` `Module.End.coe_pow` `Set.MapsTo.iterate` `Module.End.mapsTo_genEigenspace_of_comm` `LinearMap.injOn_of_disjoint_ker` `subset_rfl` `Set.instReflSubset` `Module.End.independent_genEigenspace` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `le_top` `Nat.cast_le` `Finset.sup_le` `LinearMap.ker_noncommProd_eq_of_supIndep_ker` `iSupIndep.supIndep'` `Finset.SupIndep.antitone_fun` `Module.End.genEigenspace_nat` `Finset.sup_eq_iSup` `Finset.supIndep_iff_disjoint_erase` `Disjoint.mono_right` `Finset.sup_mono_fun` `Set.MapsTo.inter_inter` `LinearMap.injOn_iff_surjOn` `finiteDimensional_inf_right` `FiniteDimensional.finiteDimensional_submodule` `Set.InjOn.mono` `Set.inter_subset_right` `Finsupp.notMem_support_iff` `zero_mem` `mem_inf` `le_inf_iff` `iSup_le` `inf_le_left` `iSup_mono` `inf_le_right`

---

← Back to Index