Instances

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

Statistics

Metric	Count
Definitions	0
Theorems instDecompositionMonoid, instDecompositionMonoidPolynomial, of_isArtinian	3
Total	3

IsArtinianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instDecompositionMonoid 📖	mathematical	—	DecompositionMonoid SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing	—	MulEquiv.decompositionMonoid RingEquivClass.toMulEquivClass AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass instDecompositionMonoidForall UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal instIsPrincipalIdealRingOfIsSemisimpleRing instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule
instDecompositionMonoidPolynomial 📖	mathematical	—	DecompositionMonoid Polynomial CommSemiring.toSemiring CommRing.toCommSemiring SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	—	MulEquiv.decompositionMonoid RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass instFiniteMaximalSpectrum instDecompositionMonoidForall UniqueFactorizationMonoid.instDecompositionMonoid PrincipalIdealRing.to_uniqueFactorizationMonoid Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd Ideal.Quotient.isDomain Ideal.instIsTwoSided_1 Ideal.IsMaximal.isPrime' MaximalSpectrum.isMaximal EuclideanDomain.to_principal_ideal_domain

StrongRankCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isArtinian 📖	mathematical	IsArtinian Pi.addCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Pi.Function.module Semiring.toModule	StrongRankCondition	—	strongRankCondition_iff_succ RingHomInvPair.ids RingHomCompTriple.ids not_subsingleton IsArtinian.subsingleton_of_injective LinearEquiv.injective

---

← Back to Index