Nilpotent

📁 Source: Mathlib/RingTheory/Finiteness/Nilpotent.lean

Statistics

Metric	Count
Definitions	0
Theorems isNilpotent_iff, isNilpotent_iff_forall_col, isNilpotent_iff_forall_row, isNilpotent_transpose_iff, isNilpotent_iff_of_finite	5
Total	5

Matrix

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_iff 📖	mathematical	—	IsNilpotent Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring mulVec Pi.instZero	—	RingHomInvPair.ids Function.smulCommClass Algebra.to_smulCommClass Module.Finite.pi Finite.of_fintype Module.Finite.self
isNilpotent_iff_forall_col 📖	mathematical	—	IsNilpotent Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring col Pi.instZero	—	isNilpotent_transpose_iff isNilpotent_iff_forall_row
isNilpotent_iff_forall_row 📖	mathematical	—	IsNilpotent Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring row Pi.instZero	—	isNilpotent_transpose_iff isNilpotent_iff mulVec_single one_smul pow_row_eq_zero_of_le Finite.le_ciSup Finite.of_fintype mulVec_eq_sum Finset.sum_congr transpose_pow transpose_transpose smul_zero Finset.sum_const_zero
isNilpotent_transpose_iff 📖	mathematical	—	IsNilpotent Matrix zero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring transpose	—	—

Module.End

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_iff_of_finite 📖	mathematical	—	IsNilpotent Module.End CommSemiring.toSemiring LinearMap.instZero RingHom.id Semiring.toNonAssocSemiring Monoid.toNatPow instMonoid DFunLike.coe LinearMap.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	Module.Finite.fg_top LinearMap.ext Submodule.span_induction pow_map_zero_of_le Finset.le_sup map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass map_add SemilinearMapClass.toAddHomClass add_zero map_smul SemilinearMapClass.toMulActionSemiHomClass smul_zero

---

← Back to Index