Noetherian

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

Statistics

Metric	Count
Definitions	0
Theorems of_isDomain, of_isLocalRing, of_isTorsionFree, of_le_jacobson, instIsHausdorffMaximalIdeal	5
Total	5

IsHausdorff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isDomain 📖	mathematical	—	IsHausdorff Ring.toAddCommGroup CommRing.toRing Semiring.toModule CommSemiring.toSemiring CommRing.toCommSemiring	—	of_isTorsionFree Module.Finite.self instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors NoZeroDivisors.toNoZeroSMulDivisors IsDomain.to_noZeroDivisors
of_isLocalRing 📖	mathematical	—	IsHausdorff	—	of_le_jacobson LE.le.trans IsLocalRing.le_maximalIdeal IsLocalRing.maximalIdeal_le_jacobson
of_isTorsionFree 📖	mathematical	—	IsHausdorff	—	IsScalarTower.left IsScalarTower.right Eq.le Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree
of_le_jacobson 📖	mathematical	Ideal CommSemiring.toSemiring CommRing.toCommSemiring Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Ideal.jacobson CommRing.toRing Bot.bot Ring.toSemiring Submodule.instBot	IsHausdorff	—	IsScalarTower.left IsScalarTower.right Eq.le Ideal.iInf_pow_smul_eq_bot_of_le_jacobson

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsHausdorffMaximalIdeal 📖	mathematical	—	IsHausdorff IsLocalRing.maximalIdeal CommRing.toCommSemiring	—	IsHausdorff.of_le_jacobson IsLocalRing.maximalIdeal_le_jacobson

---

← Back to Index