Ring

📁 Source: Mathlib/RingTheory/Artinian/Ring.lean

Statistics

Metric	Count
Definitions	0
Theorems instLocalization, isField_of_isReduced_of_isLocalRing, isNilpotent_jacobson_bot, isNilpotent_nilradical, jacobson_eq_radical, localization_artinian, localization_surjective	7
Total	7

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLocalization 📖	mathematical	—	IsArtinianRing Localization CommRing.toCommMonoid OreLocalization.instSemiring CommSemiring.toSemiring CommRing.toCommSemiring OreLocalization.oreSetComm	—	localization_artinian Localization.isLocalization
isField_of_isReduced_of_isLocalRing 📖	mathematical	—	IsField CommSemiring.toSemiring CommRing.toCommSemiring	—	MulEquiv.isField MaximalSpectrum.isMaximal Field.toIsField
isNilpotent_jacobson_bot 📖	mathematical	—	IsNilpotent Ideal Ring.toSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Module.toDistribMulAction Ideal.jacobson Bot.bot Submodule.instBot	—	IsScalarTower.left IsSemiprimaryRing.isNilpotent instIsSemiprimaryRing Ideal.jacobson_bot
isNilpotent_nilradical 📖	mathematical	—	IsNilpotent Ideal CommSemiring.toSemiring CommRing.toCommSemiring Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id nilradical	—	IsScalarTower.right nilradical.eq_1 jacobson_eq_radical isNilpotent_jacobson_bot
jacobson_eq_radical 📖	mathematical	—	Ideal.jacobson CommRing.toRing Ideal.radical CommRing.toCommSemiring	—	Ideal.radical_eq_sInf
localization_artinian 📖	mathematical	—	IsArtinianRing CommSemiring.toSemiring	—	Function.Surjective.isArtinianRing RingHom.instRingHomClass localization_surjective
localization_surjective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring RingHom.instFunLike algebraMap	—	IsLocalization.exists_mk'_eq IsArtinian.exists_pow_succ_smul_dvd IsLocalization.mk'_one IsLocalization.mk'_eq_iff_eq mul_one Submonoid.coe_one IsUnit.mul_left_cancel Submonoid.instSubmonoidClass IsLocalization.map_units map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_assoc pow_succ smul_eq_mul IsLocalization.mk'_eq_mul_mk'_one

---

← Back to Index