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_eq, finrank_maxGenEigenspace_zero_eq, hasEigenvalue_zero_tfae, isNilpotent_iff_charpoly, not_hasEigenvalue_zero_tfae	11
Total	11

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.toPow Module.End.instMonoid	LinearMap.charpoly Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Module.finrank AddCommGroup.toAddCommMonoid	—	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.toPow 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.toPow 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 instPreorderENat PartialOrder.toPreorder 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_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' Submodule.addSubgroupClass 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.toPow 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