Zero

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

Statistics

Metric	Count
Definitions	0
Theorems charpoly_eq_X_pow_finrank, charpoly_constantCoeff_eq_zero_iff, charpoly_eq_X_pow_iff, charpoly_nilpotent_tfae, finrank_eigenspace_le, finrank_genEigenspace_le, finrank_maxGenEigenspace, finrank_maxGenEigenspace_eq, finrank_maxGenEigenspace_zero_eq, hasEigenvalue_zero_tfae, isNilpotent_iff_charpoly, not_hasEigenvalue_zero_tfae	12
Total	12

IsNilpotent

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_eq_X_pow_finrank 📖	mathematical	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid	LinearMap.charpoly Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Module.finrank	—	sub_eq_zero eq_zero isReduced_of_noZeroDivisors Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Module.finrank_eq_card_chooseBasisIndex commRing_strongRankCondition IsDomain.toNontrivial Matrix.isNilpotent_charpoly_sub_pow_of_isNilpotent map smulCommClass_self IsScalarTower.left RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
charpoly_constantCoeff_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.constantCoeff charpoly Module.Free.of_divisionRing Field.toDivisionRing MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid instFunLike RingHom.id NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	List.TFAE.out smulCommClass_self IsScalarTower.left Module.Free.of_divisionRing hasEigenvalue_zero_tfae
charpoly_eq_X_pow_iff 📖	mathematical	—	charpoly Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Module.finrank AddCommGroup.toAddCommMonoid DFunLike.coe Module.End instFunLike RingHom.id Semiring.toNonAssocSemiring Module.End.instMonoid NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	List.TFAE.out charpoly_nilpotent_tfae
charpoly_nilpotent_tfae 📖	mathematical	—	List.TFAE IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid Polynomial charpoly MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Module.finrank Polynomial.natTrailingDegree	—	IsNilpotent.charpoly_eq_X_pow_finrank smulCommClass_self IsScalarTower.left map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.aeval_X aeval_self_charpoly Filter.eventually_atTop instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat eventually_iSup_ker_pow_eq ext zero_apply mem_ker le_rfl Submodule.mem_iSup_of_mem charpoly_natDegree IsDomain.toNontrivial commRing_strongRankCondition Polynomial.Monic.eq_X_pow_iff_natTrailingDegree_eq_natDegree charpoly_monic List.tfae_of_cycle
finrank_eigenspace_le 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.eigenspace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module Polynomial.rootMultiplicity DivisionRing.toRing Field.toDivisionRing charpoly Module.Free.of_divisionRing	—	finrank_genEigenspace_le
finrank_genEigenspace_le 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike DFunLike.coe OrderHom ENat PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder instLinearOrderENat Submodule.instPartialOrder OrderHom.instFunLike Module.End.genEigenspace ENat.instNatCast DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module Polynomial.rootMultiplicity DivisionRing.toRing Field.toDivisionRing charpoly Module.Free.of_divisionRing	—	le_imp_le_of_le_of_le Module.Free.of_divisionRing Submodule.finrank_mono commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing FiniteDimensional.finiteDimensional_submodule Module.End.genEigenspace_le_maximal le_refl finrank_maxGenEigenspace_eq
finrank_maxGenEigenspace 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.maxGenEigenspace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module Polynomial.natTrailingDegree charpoly Module.Free.of_divisionRing Field.toDivisionRing	—	finrank_maxGenEigenspace_zero_eq
finrank_maxGenEigenspace_eq 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.maxGenEigenspace DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module Polynomial.rootMultiplicity DivisionRing.toRing Field.toDivisionRing charpoly Module.Free.of_divisionRing	—	Module.Free.of_divisionRing smulCommClass_self Module.End.maxGenEigenspace_eq_maxGenEigenspace_zero finrank_maxGenEigenspace_zero_eq Polynomial.rootMultiplicity_eq_natTrailingDegree charpoly_sub_smul
finrank_maxGenEigenspace_zero_eq 📖	mathematical	—	Module.finrank Submodule CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Module.End.maxGenEigenspace MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Submodule.addCommMonoid Submodule.module Polynomial.natTrailingDegree charpoly Module.Free.of_divisionRing Field.toDivisionRing	—	Module.Free.of_divisionRing smulCommClass_self Module.End.genEigenspace_nat zero_smul sub_zero RingHomSurjective.ids isCompl_iSup_ker_pow_iInf_range_pow isArtinian_of_fg_of_artinian' DivisionRing.instIsArtinianRing isNoetherian_of_isNoetherianRing_of_finite IsSimpleModule.instIsNoetherian instIsSimpleModule Module.End.mul_apply pow_succ pow_succ' map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass RingHomInvPair.ids Module.Basis.ext Module.Basis.prod_apply RingHomInvPair.triples₂ RingHomCompTriple.ids map_add SemilinearMapClass.toAddHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass add_zero zero_add Module.Free.prod Module.Finite.prod FiniteDimensional.finiteDimensional_submodule LinearEquiv.charpoly_conj charpoly_prodMap Polynomial.natTrailingDegree_mul IsDomain.to_noZeroDivisors instIsDomain Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing charpoly_monic Polynomial.natTrailingDegree_eq_zero_of_constantCoeff_ne_zero List.TFAE.out IsScalarTower.left not_hasEigenvalue_zero_tfae pow_one Submodule.mem_bot IsCompl.inf_eq_bot charpoly_nilpotent_tfae isNoetherian_submodule' AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass ZeroMemClass.coe_zero pow_zero
hasEigenvalue_zero_tfae 📖	mathematical	—	List.TFAE Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring minpoly Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.constantCoeff charpoly Module.Free.of_divisionRing Field.toDivisionRing MonoidHom LinearMap RingHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Submodule Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder Bot.bot Submodule.instBot ker NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instFunLike	—	smulCommClass_self IsScalarTower.left Module.End.hasEigenvalue_iff_isRoot instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.Free.of_divisionRing minpoly_dvd_charpoly Polynomial.coeff_zero_eq_eval_zero Polynomial.eval_mul MulZeroClass.zero_mul RingHomInvPair.ids Finite.of_fintype det_toMatrix Matrix.det_eq_sign_charpoly_coeff Polynomial.constantCoeff_apply charpoly.eq_1 MulZeroClass.mul_zero bot_lt_ker_of_det_eq_zero Mathlib.Tactic.Contrapose.contrapose₁ Mathlib.Tactic.Push.not_and_eq Module.End.hasEigenvalue_of_hasEigenvector Module.End.eigenspace_zero List.tfae_of_cycle
isNilpotent_iff_charpoly 📖	mathematical	—	IsNilpotent Module.End CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow Module.End.instMonoid charpoly Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Module.finrank	—	IsNilpotent.charpoly_eq_X_pow_finrank smulCommClass_self IsScalarTower.left Polynomial.aeval_X_pow aeval_self_charpoly
not_hasEigenvalue_zero_tfae 📖	mathematical	—	List.TFAE Module.End.HasEigenvalue EuclideanDomain.toCommRing Field.toEuclideanDomain MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.IsRoot CommSemiring.toSemiring CommRing.toCommSemiring minpoly Module.End DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield 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 Semifield.toCommSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.constantCoeff charpoly Module.Free.of_divisionRing Field.toDivisionRing MonoidHom LinearMap RingHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring MonoidHom.instFunLike det Submodule ker Bot.bot Submodule.instBot	—	smulCommClass_self IsScalarTower.left Module.Free.of_divisionRing List.TFAE.not hasEigenvalue_zero_tfae not_imp_not bot_lt_iff_ne_bot Mathlib.Tactic.Push.not_and_eq

---

← Back to Index