HopkinsLevitzki

📁 Source: Mathlib/RingTheory/HopkinsLevitzki.lean

Statistics

Metric	Count
Definitions	0
Theorems isArtinianRing_of_krullDimLE_zero, finite_of_isArtinian, finite_of_isNoetherian, induction, isNoetherianRing_iff_jacobson_fg, isNoetherian_iff_finite_of_jacobson_fg, isNoetherian_iff_isArtinian, instIsNoetherianRingOfIsArtinianRing, isArtinianRing_iff_isFiniteLength, isArtinianRing_iff_isNilpotent_maximalIdeal, isArtinianRing_iff_isNoetherianRing_krullDimLE_zero, isArtinianRing_iff_krullDimLE_zero, isNoetherian_of_finite_isArtinian	13
Total	13

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isArtinianRing_of_krullDimLE_zero 📖	mathematical	—	IsArtinianRing CommSemiring.toSemiring CommRing.toCommSemiring	—	Ring.jacobson_eq_nilradical_of_krullDimLE_zero Set.Finite.subset minimalPrimes.finite_of_isNoetherianRing Ideal.mem_minimalPrimes_of_krullDimLE_zero instIsMaximalOfIsPrimeOfKrullDimLEOfNatNat IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule nilradical_eq_sInf sInf_eq_iInf' RingEquiv.isSemisimpleRing Ideal.isCoprime_of_isMaximal Subtype.coe_ne_coe instIsSemisimpleRingForallOfFinite IsScalarTower.left isNilpotent_nilradical IsSemiprimaryRing.isNoetherian_iff_isArtinian

IsSemiprimaryRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finite_of_isArtinian 📖	mathematical	—	Module.Finite Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Ring.instIsTwoSidedJacobson
finite_of_isNoetherian 📖	mathematical	—	Module.Finite Ring.toSemiring AddCommGroup.toAddCommMonoid	—	Ring.instIsTwoSidedJacobson
induction 📖	—	—	—	—	IsScalarTower.left Ring.instIsTwoSidedJacobson isSemiprimaryRing_iff bot_le SetLike.coe_subset_coe instIsConcreteLE Module.isTorsionBySet_iff_subset_annihilator LinearMap.isSemisimpleModule_iff_of_bijective Ideal.Quotient.instRingHomSurjectiveQuotientMk Function.bijective_id IsSemisimpleRing.isSemisimpleModule LE.le.trans le_top Ideal.one_eq_top Submodule.pow_zero Submodule.pow_one Submodule.isScalarTower' Submodule.le_annihilator_iff Submodule.mul_smul Submodule.pow_succ Submodule.annihilator_top Submodule.Quotient.isScalarTower Module.isTorsionBySet_quotient_iff Submodule.smul_mem_smul Ideal.pow_le_self
isNoetherianRing_iff_jacobson_fg 📖	mathematical	—	IsNoetherianRing Ring.toSemiring Ideal.FG Ring.jacobson	—	IsNoetherian.noetherian isNoetherian_iff_finite_of_jacobson_fg Module.Finite.self
isNoetherian_iff_finite_of_jacobson_fg 📖	mathematical	Ideal.FG Ring.toSemiring Ring.jacobson	IsNoetherian AddCommGroup.toAddCommMonoid Module.Finite	—	Module.IsNoetherian.finite induction IsScalarTower.left List.TFAE.out IsSemisimpleModule.finite_tfae isNoetherian_iff_submodule_quotient Module.Finite.of_fg Submodule.FG.smul Ring.instIsTwoSidedJacobson Module.Finite.fg_top Module.Finite.quotient
isNoetherian_iff_isArtinian 📖	mathematical	—	IsNoetherian Ring.toSemiring AddCommGroup.toAddCommMonoid IsArtinian	—	induction IsScalarTower.left List.TFAE.out IsSemisimpleModule.finite_tfae isNoetherian_iff_submodule_quotient isArtinian_iff_submodule_quotient

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsNoetherianRingOfIsArtinianRing 📖	mathematical	—	IsNoetherianRing Ring.toSemiring	—	List.TFAE.out IsArtinianRing.tfae
isArtinianRing_iff_isFiniteLength 📖	mathematical	—	IsArtinianRing Ring.toSemiring IsFiniteLength Ring.toAddCommGroup Semiring.toModule	—	List.TFAE.out IsArtinianRing.tfae isFiniteLength_iff_isNoetherian_isArtinian
isArtinianRing_iff_isNilpotent_maximalIdeal 📖	mathematical	—	IsArtinianRing CommSemiring.toSemiring CommRing.toCommSemiring IsNilpotent Ideal Submodule.pointwiseZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Submodule.instPowNat IsScalarTower.right Algebra.id IsLocalRing.maximalIdeal	—	IsScalarTower.right isArtinianRing_iff_krullDimLE_zero Ideal.FG.isNilpotent_iff_le_nilradical IsNoetherian.noetherian List.TFAE.out Ring.krullDimLE_zero_and_isLocalRing_tfae IsLocalRing.isMaximal_iff le_antisymm_iff IsLocalRing.le_maximalIdeal Ideal.instNontrivial IsLocalRing.toNontrivial
isArtinianRing_iff_isNoetherianRing_krullDimLE_zero 📖	mathematical	—	IsArtinianRing CommSemiring.toSemiring CommRing.toCommSemiring IsNoetherianRing Ring.KrullDimLE	—	instIsNoetherianRingOfIsArtinianRing PrimeSpectrum.instKrullDimLEOfNatNat IsNoetherianRing.isArtinianRing_of_krullDimLE_zero
isArtinianRing_iff_krullDimLE_zero 📖	mathematical	—	IsArtinianRing CommSemiring.toSemiring CommRing.toCommSemiring Ring.KrullDimLE	—	isArtinianRing_iff_isNoetherianRing_krullDimLE_zero
isNoetherian_of_finite_isArtinian 📖	mathematical	—	IsNoetherian CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid	—	Submodule.fg_def Module.finite_def isNoetherian_top_iff Submodule.span_iUnion Set.iUnion_of_singleton_coe RingHomSurjective.ids LinearMap.span_singleton_eq_range LinearEquiv.isNoetherian_iff Ideal.instIsTwoSided_1 LinearMap.isNoetherian_iff_of_bijective Ideal.Quotient.instRingHomSurjectiveQuotientMk Function.bijective_id instIsNoetherianRingOfIsArtinianRing IsArtinianRing.eq_1 LinearMap.isArtinian_iff_of_bijective LinearEquiv.isArtinian_iff isArtinian_submodule' isNoetherian_iSup Set.finite_coe_iff

---

← Back to Index