Nilpotent

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

Statistics

Metric	Count
Definitions	0
Theorems isNilpotent_iff_le_nilradical, isNilpotent_nilradical	2
Total	2

Ideal.FG

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_iff_le_nilradical 📖	mathematical	Ideal.FG CommSemiring.toSemiring	IsNilpotent Ideal Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder nilradical	—	IsScalarTower.right Ideal.pow_mem_pow Ideal.exists_pow_le_of_le_radical_of_fg le_bot_iff

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isNilpotent_nilradical 📖	mathematical	—	IsNilpotent Ideal CommSemiring.toSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id nilradical	—	IsScalarTower.right Ideal.exists_radical_pow_le_of_fg IsNoetherian.noetherian eq_bot_iff

---

← Back to Index