Module

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

Statistics

Metric	Count
Definitions `IsArtinian`, `IsArtinianRing`, `equivPi`, `fieldOfSubtypeIsMaximal`, `primeSpectrumEquivMaximalSpectrum`, `quotNilradicalEquivPi`	6
Theorems `instIsArtinianRing`, `instIsArtinianRing`, `isArtinianRing`, `bijective_of_injective_endomorphism`, `disjoint_partial_infs_eventually_top`, `eventuallyConst_of_isArtinian`, `exists_pow_succ_smul_dvd`, `finite_of_linearIndependent`, `induction`, `isSemisimpleModule_iff_jacobson`, `monotone_stabilizes`, `range_smul_pow_stabilizes`, `set_has_minimal`, `subsingleton_of_injective`, `surjective_of_injective_endomorphism`, `instFiniteMaximalSpectrum`, `instFinitePrimeSpectrum`, `instIsSemiprimaryRing`, `isField_of_isDomain`, `isMaximal_of_isPrime`, `isPrime_iff_isMaximal`, `isSemisimpleRing_iff_jacobson`, `isSemisimpleRing_of_isReduced`, `isUnitSubmonoid_eq`, `isUnitSubmonoid_eq_nonZeroDivisorsRight`, `isUnitSubmonoid_eq_of_mulOpposite`, `isUnit_iff_isLeftRegular`, `isUnit_iff_isRegular`, `isUnit_iff_isRegular_of_mulOpposite`, `isUnit_iff_isRightRegular`, `isUnit_iff_mem_nonZeroDivisors`, `isUnit_iff_mem_nonZeroDivisors_of_mulOpposite`, `isUnit_of_mem_nonZeroDivisors`, `isUnit_of_mem_nonZeroDivisors_of_mulOpposite`, `isUnit_submonoid_eq`, `nonZeroDivisorsLeft_eq_isUnitSubmonoid`, `of_finite`, `primeSpectrumEquivMaximalSpectrum_apply_asIdeal`, `primeSpectrumEquivMaximalSpectrum_comp_asIdeal`, `primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal`, `primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal`, `primeSpectrum_asIdeal_range_eq`, `setOf_isMaximal_finite`, `setOf_isPrime_finite`, `isArtinian_iff`, `eventually_codisjoint_ker_pow_range_pow`, `eventually_iInf_range_pow_eq`, `eventually_isCompl_ker_pow_range_pow`, `isArtinian_iff_of_bijective`, `isCompl_iSup_ker_pow_iInf_range_pow`, `isArtinian_of_zero_eq_one`, `isArtinianRing`, `instIsArtinianRingForallOfFinite`, `instIsArtinianRingMatrix`, `instIsArtinianRingProd`, `instIsArtinianRingQuotientIdeal`, `instIsDedekindFiniteMonoidOfIsArtinianRing`, `instIsNoetherianRingMatrix`, `isArtinianRing_iff`, `isArtinianRing_range`, `isArtinianRing_rangeS`, `isArtinian_finsupp`, `isArtinian_iSup`, `isArtinian_iff`, `isArtinian_iff_submodule_quotient`, `isArtinian_of_fg_of_artinian`, `isArtinian_of_fg_of_artinian'`, `isArtinian_of_finite`, `isArtinian_of_injective`, `isArtinian_of_le`, `isArtinian_of_linearEquiv`, `isArtinian_of_quotient_of_artinian`, `isArtinian_of_range_eq_ker`, `isArtinian_of_submodule_of_artinian`, `isArtinian_of_surjective`, `isArtinian_of_surjective_algebraMap`, `isArtinian_of_tower`, `isArtinian_pi`, `isArtinian_pi'`, `isArtinian_prod`, `isArtinian_range`, `isArtinian_span_of_finite`, `isArtinian_submodule'`, `isArtinian_sup`, `monotone_stabilizes_iff_artinian`, `set_has_minimal_iff_artinian`	86
Total	92

DivisionRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsArtinianRing` 📖	mathematical	—	`IsArtinianRing` `DivisionSemiring.toSemiring` `toDivisionSemiring`	—	`DivisionSemiring.instIsArtinianRing`

DivisionSemiring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsArtinianRing` 📖	mathematical	—	`IsArtinianRing` `toSemiring`	—	`Finite.wellFounded_of_trans_of_irrefl` `Ideal.instFinite` `instIsTransLt` `instIrreflLt`

Function.Surjective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinianRing` 📖	mathematical	`DFunLike.coe`	`IsArtinianRing`	—	`isArtinianRing_iff` `OrderEmbedding.wellFounded` `IsWellFounded.wf`

IsArtinian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bijective_of_injective_endomorphism` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`Function.Bijective`	—	`surjective_of_injective_endomorphism`
`disjoint_partial_infs_eventually_top` 📖	mathematical	`Disjoint` `OrderDual` `Submodule` `OrderDual.instPartialOrder` `Submodule.instPartialOrder` `OrderDual.instOrderBot` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instOrderTop` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `SemilatticeSup.toPartialOrder` `OrderDual.instSemilatticeSup` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `OrderHom.instFunLike` `partialSups` `LocallyFiniteOrder.toLocallyFiniteOrderBot` `Nat.instOrderBot` `Nat.instLocallyFiniteOrder` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `OrderDual.toDual`	`Top.top` `Submodule.instTop`	—	`monotone_stabilizes` `Disjoint.eq_bot_of_ge` `sup_eq_left` `partialSups_add_one` `le_add_right` `Nat.instCanonicallyOrderedAdd`
`eventuallyConst_of_isArtinian` 📖	mathematical	—	`Filter.EventuallyConst` `OrderDual` `Submodule` `DFunLike.coe` `OrderHom` `Nat.instPreorder` `OrderDual.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `Filter.atTop`	—	`monotone_stabilizes`
`exists_pow_succ_smul_dvd` 📖	mathematical	—	`SMulZeroClass.toSMul` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddCommMonoid.toAddMonoid` `DistribSMul.toSMulZeroClass` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `Module.toDistribMulAction` `Monoid.toNatPow`	—	`RingHomSurjective.ids` `smulCommClass_self` `range_smul_pow_stabilizes`
`finite_of_linearIndependent` 📖	mathematical	`LinearIndependent` `Set` `Set.instMembership`	`Set.Finite`	—	`WellFoundedLT.finite_of_iSupIndep` `LinearIndependent.iSupIndep_span_singleton` `LinearIndependent.ne_zero`
`induction` 📖	—	—	—	—	`WellFoundedLT.induction`
`isSemisimpleModule_iff_jacobson` 📖	mathematical	—	`IsSemisimpleModule` `Module.jacobson` `Bot.bot` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instBot`	—	`IsSemisimpleModule.jacobson_eq_bot` `Finset.exists_inf_le` `isSimpleModule_iff_isCoatom` `IsSemisimpleModule.of_injective` `instIsSemisimpleModuleForallOfFinite` `Finite.of_fintype` `instIsSemisimpleModuleOfIsSimpleModule` `LinearMap.ker_eq_bot` `le_bot_iff` `Module.jacobson.eq_1` `Submodule.mem_sInf` `Submodule.mem_finsetInf` `Submodule.Quotient.mk_eq_zero`
`monotone_stabilizes` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderDual` `Submodule` `Nat.instPreorder` `OrderDual.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderHom.instFunLike`	—	`monotone_stabilizes_iff_artinian`
`range_smul_pow_stabilizes` 📖	mathematical	—	`LinearMap.range` `CommSemiring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap` `LinearMap.instSMul` `DistribMulAction.toDistribSMul` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AddCommMonoid.toAddMonoid` `Module.toDistribMulAction` `smulCommClass_self` `CommSemiring.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `Monoid.toNatPow` `LinearMap.id`	—	`monotone_stabilizes` `RingHomSurjective.ids` `smulCommClass_self` `smul_assoc` `IsScalarTower.left` `smul_eq_mul` `pow_add` `add_tsub_cancel_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub`
`set_has_minimal` 📖	mathematical	`Set.Nonempty` `Submodule`	`Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`set_has_minimal_iff_artinian`
`subsingleton_of_injective` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `Prod.instAddCommMonoid` `Prod.instModule` `LinearMap.instFunLike`	—	—	`RingHomCompTriple.ids` `surjective_of_injective_endomorphism` `Prod.mk_right_injective`
`surjective_of_injective_endomorphism` 📖	—	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	—	—	`Mathlib.Tactic.Contrapose.contrapose₁` `eq_1` `WellFoundedLT.eq_1` `isWellFounded_iff` `RelEmbedding.not_wellFounded` `instIsStrictOrderLt` `RingHomSurjective.ids` `LinearMap.range.congr_simp` `pow_succ` `RingHomCompTriple.ids` `LinearMap.range_comp` `Submodule.map_top` `Submodule.map_strictMono_of_injective` `Module.End.iterate_injective` `Ne.lt_top` `LinearMap.range_eq_top`

IsArtinianRing

Definitions

Name	Category	Theorems
`equivPi` 📖	CompOp	—
`fieldOfSubtypeIsMaximal` 📖	CompOp	—
`primeSpectrumEquivMaximalSpectrum` 📖	CompOp	4 math math: `primeSpectrumEquivMaximalSpectrum_apply_asIdeal`, `primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal`, `primeSpectrumEquivMaximalSpectrum_comp_asIdeal`, `primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal`
`quotNilradicalEquivPi` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteMaximalSpectrum` 📖	mathematical	—	`Finite` `MaximalSpectrum`	—	`Finite.of_equiv` `Set.Finite.to_subtype` `setOf_isMaximal_finite`
`instFinitePrimeSpectrum` 📖	mathematical	—	`Finite` `PrimeSpectrum` `CommRing.toCommSemiring`	—	`Finite.of_equiv` `Set.Finite.to_subtype` `setOf_isPrime_finite`
`instIsSemiprimaryRing` 📖	mathematical	—	`IsSemiprimaryRing`	—	`Ring.instIsTwoSidedJacobson` `isSemisimpleRing_iff_jacobson` `instIsArtinianRingQuotientIdeal` `Ring.jacobson_quotient_jacobson` `IsScalarTower.left` `Ideal.pow_le_pow_right` `IsArtinian.monotone_stabilizes` `Ideal.IsTwoSided.pow_succ` `WellFounded.has_min` `wellFounded_lt` `Submodule.pow_zero` `Submodule.one_mul` `Submodule.pow_succ` `mul_assoc` `RingHomSurjective.ids` `Ideal.span.eq_1` `LinearMap.span_singleton_eq_range` `LinearMap.map_le_range` `Mathlib.Tactic.Contrapose.contrapose₂` `Mathlib.Tactic.Push.not_and_eq` `le_bot_iff` `Ideal.mul_le` `LE.le.eq_of_not_lt` `LE.le.trans` `Ideal.span_singleton_le_iff_mem` `smul_eq_mul` `Submodule.map_smul''` `le_antisymm` `Eq.trans_le` `Submodule.FG.eq_bot_of_le_jacobson_smul` `Submodule.fg_span` `Set.finite_singleton` `le_refl`
`isField_of_isDomain` 📖	mathematical	—	`IsField` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Nontrivial.exists_pair_ne` `IsDomain.toNontrivial` `mul_comm` `IsArtinian.exists_pow_succ_smul_dvd` `mul_sub` `sub_eq_zero` `pow_add` `pow_one` `mul_assoc` `mul_eq_zero` `IsDomain.to_noZeroDivisors` `pow_ne_zero` `isReduced_of_noZeroDivisors`
`isMaximal_of_isPrime` 📖	mathematical	—	`Ideal.IsMaximal` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	`Ideal.Quotient.maximal_of_isField` `isField_of_isDomain` `instIsArtinianRingQuotientIdeal` `Ideal.instIsTwoSided_1` `Ideal.Quotient.isDomain`
`isPrime_iff_isMaximal` 📖	mathematical	—	`Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.IsMaximal`	—	`isMaximal_of_isPrime` `Ideal.IsMaximal.isPrime`
`isSemisimpleRing_iff_jacobson` 📖	mathematical	—	`IsSemisimpleRing` `Ring.jacobson` `Bot.bot` `Ideal` `Ring.toSemiring` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`IsArtinian.isSemisimpleModule_iff_jacobson`
`isSemisimpleRing_of_isReduced` 📖	mathematical	—	`IsSemisimpleRing` `CommRing.toRing`	—	`RingEquiv.isSemisimpleRing` `instIsSemisimpleRingForallOfFinite` `instFiniteMaximalSpectrum` `instIsSemisimpleModuleOfIsSimpleModule` `instIsSimpleModule`
`isUnitSubmonoid_eq` 📖	mathematical	—	`IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisors`	—	`Submonoid.ext`
`isUnitSubmonoid_eq_nonZeroDivisorsRight` 📖	mathematical	—	`IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisorsRight`	—	`Submonoid.ext` `isRightRegular_iff_mem_nonZeroDivisorsRight` `isUnit_iff_isRightRegular`
`isUnitSubmonoid_eq_of_mulOpposite` 📖	mathematical	—	`IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisors`	—	`Submonoid.ext`
`isUnit_iff_isLeftRegular` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsLeftRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isRightRegular_op` `isUnit_op` `isUnit_iff_isRightRegular`
`isUnit_iff_isRegular` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isRegular_iff` `isUnit_iff_isRightRegular` `IsRegular.left` `IsUnit.isRegular`
`isUnit_iff_isRegular_of_mulOpposite` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`isRegular_iff` `isUnit_iff_isLeftRegular` `IsRegular.right` `IsUnit.isRegular`
`isUnit_iff_isRightRegular` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `IsRightRegular` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`IsRightRegular.eq_1` `IsUnit.isUnit_iff_mulRight_bijective` `Function.Bijective.eq_1` `IsArtinian.surjective_of_injective_endomorphism`
`isUnit_iff_mem_nonZeroDivisors` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`isUnit_iff_isRegular` `isRegular_iff_mem_nonZeroDivisors`
`isUnit_iff_mem_nonZeroDivisors_of_mulOpposite` 📖	mathematical	—	`IsUnit` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	—	`isUnit_iff_isRegular_of_mulOpposite` `isRegular_iff_mem_nonZeroDivisors`
`isUnit_of_mem_nonZeroDivisors` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsUnit` `MonoidWithZero.toMonoid`	—	`isUnit_iff_isRegular` `isRegular_iff_mem_nonZeroDivisors`
`isUnit_of_mem_nonZeroDivisors_of_mulOpposite` 📖	mathematical	`Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Ring.toSemiring` `SetLike.instMembership` `Submonoid.instSetLike` `nonZeroDivisors`	`IsUnit` `MonoidWithZero.toMonoid`	—	`isUnit_iff_isRegular_of_mulOpposite` `isRegular_iff_mem_nonZeroDivisors`
`isUnit_submonoid_eq` 📖	mathematical	—	`IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisors`	—	`isUnitSubmonoid_eq`
`nonZeroDivisorsLeft_eq_isUnitSubmonoid` 📖	mathematical	—	`IsUnit.submonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `nonZeroDivisorsLeft`	—	`Submonoid.ext` `isLeftRegular_iff_mem_nonZeroDivisorsLeft` `isUnit_iff_isLeftRegular`
`of_finite` 📖	mathematical	—	`IsArtinianRing` `Ring.toSemiring`	—	`isArtinian_of_tower` `isArtinian_of_fg_of_artinian'`
`primeSpectrumEquivMaximalSpectrum_apply_asIdeal` 📖	mathematical	—	`MaximalSpectrum.asIdeal` `CommRing.toCommSemiring` `DFunLike.coe` `Equiv` `PrimeSpectrum` `MaximalSpectrum` `EquivLike.toFunLike` `Equiv.instEquivLike` `primeSpectrumEquivMaximalSpectrum` `PrimeSpectrum.asIdeal`	—	—
`primeSpectrumEquivMaximalSpectrum_comp_asIdeal` 📖	mathematical	—	`PrimeSpectrum` `CommRing.toCommSemiring` `MaximalSpectrum` `Ideal` `CommSemiring.toSemiring` `MaximalSpectrum.asIdeal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `primeSpectrumEquivMaximalSpectrum` `PrimeSpectrum.asIdeal`	—	—
`primeSpectrumEquivMaximalSpectrum_symm_apply_asIdeal` 📖	mathematical	—	`PrimeSpectrum.asIdeal` `CommRing.toCommSemiring` `DFunLike.coe` `Equiv` `MaximalSpectrum` `PrimeSpectrum` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `primeSpectrumEquivMaximalSpectrum` `MaximalSpectrum.asIdeal`	—	—
`primeSpectrumEquivMaximalSpectrum_symm_comp_asIdeal` 📖	mathematical	—	`MaximalSpectrum` `CommRing.toCommSemiring` `PrimeSpectrum` `Ideal` `CommSemiring.toSemiring` `PrimeSpectrum.asIdeal` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `Equiv.symm` `primeSpectrumEquivMaximalSpectrum` `MaximalSpectrum.asIdeal`	—	—
`primeSpectrum_asIdeal_range_eq` 📖	mathematical	—	`Set.range` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PrimeSpectrum` `PrimeSpectrum.asIdeal` `MaximalSpectrum` `MaximalSpectrum.asIdeal`	—	`PrimeSpectrum.range_asIdeal` `MaximalSpectrum.range_asIdeal`
`setOf_isMaximal_finite` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `setOf` `Ideal.IsMaximal`	—	`Finset.exists_inf_le` `Set.finite_def` `Ideal.IsPrime.inf_le'` `Ideal.IsMaximal.isPrime` `Ideal.IsMaximal.eq_of_le` `Ideal.IsMaximal.ne_top`
`setOf_isPrime_finite` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `setOf` `Ideal.IsPrime`	—	`setOf_isMaximal_finite`

LinearEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinian_iff` 📖	mathematical	—	`IsArtinian`	—	`RingHomInvPair.ids` `isArtinian_of_linearEquiv`

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eventually_codisjoint_ker_pow_range_pow` 📖	mathematical	—	`Filter.Eventually` `Codisjoint` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `Submodule.instOrderTop` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `LinearMap` `Monoid.toNatPow` `Module.End.instMonoid` `range` `RingHomSurjective.ids` `Filter.atTop` `Nat.instPreorder`	—	`RingHomSurjective.ids` `IsArtinian.monotone_stabilizes` `Filter.eventually_atTop` `SemilatticeSup.instIsDirectedOrder` `codisjoint_iff` `Module.End.pow_apply` `mem_range` `mem_range_self` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `semilinearMapClass` `sub_self` `sub_add_cancel`
`eventually_iInf_range_pow_eq` 📖	mathematical	—	`Filter.Eventually` `Submodule` `iInf` `Submodule.instInfSet` `range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Module.End` `LinearMap` `Monoid.toNatPow` `Module.End.instMonoid` `Filter.atTop` `Nat.instPreorder`	—	`RingHomSurjective.ids` `IsArtinian.monotone_stabilizes` `Filter.eventually_atTop` `SemilatticeSup.instIsDirectedOrder` `le_antisymm` `iInf_le` `le_iInf` `le_or_gt` `LE.le.trans` `le_refl` `OrderHom.monotone` `LT.lt.le`
`eventually_isCompl_ker_pow_range_pow` 📖	mathematical	—	`Filter.Eventually` `IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `Module.End` `LinearMap` `Monoid.toNatPow` `Module.End.instMonoid` `range` `RingHomSurjective.ids` `Filter.atTop` `Nat.instPreorder`	—	`Filter.mp_mem` `RingHomSurjective.ids` `Filter.Eventually.and` `Module.End.eventually_disjoint_ker_pow_range_pow` `eventually_codisjoint_ker_pow_range_pow` `Filter.univ_mem'`
`isArtinian_iff_of_bijective` 📖	mathematical	`Function.Bijective` `DFunLike.coe` `LinearMap` `instFunLike`	`IsArtinian`	—	`StrictMono.wellFoundedLT` `OrderIso.strictMono`
`isCompl_iSup_ker_pow_iInf_range_pow` 📖	mathematical	—	`IsCompl` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.instPartialOrder` `CompleteLattice.toBoundedOrder` `Submodule.completeLattice` `iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `ker` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap` `Monoid.toNatPow` `Module.End.instMonoid` `iInf` `Submodule.instInfSet` `range` `RingHomSurjective.ids`	—	`RingHomSurjective.ids` `Filter.eventually_atTop` `SemilatticeSup.instIsDirectedOrder` `Filter.Eventually.and` `eventually_isCompl_ker_pow_range_pow` `eventually_iInf_range_pow_eq` `eventually_iSup_ker_pow_eq` `le_refl`

Ring

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinian_of_zero_eq_one` 📖	mathematical	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne`	`IsArtinianRing`	—	`subsingleton_of_zero_eq_one` `Finite.to_wellFoundedLT` `Finite.of_fintype`

RingEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isArtinianRing` 📖	mathematical	—	`IsArtinianRing`	—	`Function.Surjective.isArtinianRing` `RingEquivClass.toRingHomClass` `instRingEquivClass` `surjective`

(root)

Definitions

Name	Category	Theorems
`IsArtinian` 📖	MathDef	33 math math: `isArtinian_iff`, `isArtinian_iff_submodule_quotient`, `isArtinian_of_le`, `isArtinian_of_fg_of_artinian'`, `isArtinian_prod`, `isArtinian_span_of_finite`, `isArtinian_of_quotient_of_artinian`, `isArtinian_range`, `isArtinian_of_surjective_algebraMap`, `isArtinian_of_fg_of_artinian`, `isArtinian_of_submodule_of_artinian`, `LieSubmodule.instIsArtinianSubtypeMem`, `IsSemisimpleModule.finite_tfae`, `set_has_minimal_iff_artinian`, `isArtinianRing_iff`, `isArtinian_of_tower`, `isArtinian_submodule'`, `IsArtinianRing.tfae`, `isArtinian_of_injective`, `LinearMap.isArtinian_iff_of_bijective`, `isArtinian_of_range_eq_ker`, `isArtinian_of_surjective`, `isArtinian_finsupp`, `monotone_stabilizes_iff_artinian`, `isArtinian_sup`, `IsSemiprimaryRing.isNoetherian_iff_isArtinian`, `isArtinian_of_finite`, `isFiniteLength_iff_isNoetherian_isArtinian`, `isArtinian_of_linearEquiv`, `LieSubalgebra.instIsArtinianSubtypeMem`, `isArtinian_pi'`, `instIsArtinianOfIsSemisimpleModuleOfFinite`, `LinearEquiv.isArtinian_iff`
`IsArtinianRing` 📖	MathDef	30 math math: `AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_presheaf_obj`, `Function.Surjective.isArtinianRing`, `IsSimpleRing.tfae`, `Module.finite_iff_isArtinianRing`, `AlgebraicGeometry.isLocallyArtinian_iff_of_isOpenCover`, `DivisionRing.instIsArtinianRing`, `AlgebraicGeometry.IsLocallyArtinian.isArtinianRing_of_isAffine`, `isArtinianRing_rangeS`, `isArtinianRing_iff_isNoetherianRing_krullDimLE_zero`, `IsSimpleRing.isSemisimpleRing_iff_isArtinianRing`, `DivisionSemiring.instIsArtinianRing`, `IsArtinianRing.of_finite`, `RingEquiv.isArtinianRing`, `isArtinianRing_iff`, `IsArtinianRing.instLocalization`, `instIsArtinianRingQuotientIdeal`, `IsNoetherianRing.isArtinianRing_of_krullDimLE_zero`, `isArtinianRing_iff_isNilpotent_maximalIdeal`, `isArtinianRing_range`, `isSimpleRing_isArtinianRing_iff`, `isArtinianRing_iff_isFiniteLength`, `Ring.isArtinian_of_zero_eq_one`, `AlgebraicGeometry.Scheme.isLocallyArtinianScheme_Spec`, `Algebra.QuasiFinite.instIsArtinianRingFiber`, `AlgebraicGeometry.Scheme.isArtinianScheme_Spec`, `instIsArtinianRingMatrix`, `isArtinianRing_iff_krullDimLE_zero`, `instIsArtinianRingProd`, `IsArtinianRing.localization_artinian`, `IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsArtinianRingForallOfFinite` 📖	mathematical	`IsArtinianRing`	`Pi.semiring`	—	`Finite.induction_empty_option` `RingEquiv.isArtinianRing` `Finite.to_wellFoundedLT` `Finite.of_fintype` `Unique.instSubsingleton` `PEmpty.instIsEmpty` `instIsArtinianRingProd`
`instIsArtinianRingMatrix` 📖	mathematical	—	`IsArtinianRing` `Matrix` `Matrix.semiring` `Ring.toSemiring`	—	`IsArtinianRing.of_finite` `Matrix.Semiring.isScalarTower` `IsScalarTower.left` `Module.Finite.matrix` `Module.Free.self` `Module.Finite.self` `Finite.of_fintype`
`instIsArtinianRingProd` 📖	mathematical	—	`IsArtinianRing` `Prod.instSemiring`	—	`OrderEmbedding.wellFoundedLT` `Prod.wellFoundedLT`
`instIsArtinianRingQuotientIdeal` 📖	mathematical	—	`IsArtinianRing` `HasQuotient.Quotient` `Ideal` `Ring.toSemiring` `Ideal.instHasQuotient` `Ideal.Quotient.ring`	—	`isArtinian_of_tower` `Ideal.Quotient.isScalarTower_right` `isArtinian_of_quotient_of_artinian`
`instIsDedekindFiniteMonoidOfIsArtinianRing` 📖	mathematical	—	`IsDedekindFiniteMonoid` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring`	—	`IsArtinian.surjective_of_injective_endomorphism` `isRightRegular_of_mul_eq_one` `left_inv_eq_right_inv`
`instIsNoetherianRingMatrix` 📖	mathematical	—	`IsNoetherianRing` `Matrix` `Matrix.semiring` `Ring.toSemiring`	—	`IsNoetherianRing.of_finite` `Matrix.Semiring.isScalarTower` `IsScalarTower.left` `Module.Finite.matrix` `Module.Free.self` `Module.Finite.self` `Finite.of_fintype`
`isArtinianRing_iff` 📖	mathematical	—	`IsArtinianRing` `IsArtinian` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	—
`isArtinianRing_range` 📖	mathematical	—	`IsArtinianRing` `Subring` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `Ring.toSemiring` `Subring.toRing`	—	`isArtinianRing_rangeS`
`isArtinianRing_rangeS` 📖	mathematical	—	`IsArtinianRing` `Subsemiring` `Semiring.toNonAssocSemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `Subsemiring.toSemiring`	—	`Function.Surjective.isArtinianRing` `RingHom.instRingHomClass` `RingHom.rangeSRestrict_surjective`
`isArtinian_finsupp` 📖	mathematical	—	`IsArtinian` `Finsupp` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toSemiring` `Finsupp.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Finsupp.module`	—	`isArtinian_of_linearEquiv` `RingHomInvPair.ids` `isArtinian_pi'`
`isArtinian_iSup` 📖	mathematical	`IsArtinian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	`iSup` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice`	—	`Finite.induction_empty_option` `Equiv.iSup_comp` `iSup_of_empty` `PEmpty.instIsEmpty` `Finite.to_wellFoundedLT` `Finite.of_fintype` `Unique.instSubsingleton` `iSup_option` `isArtinian_sup`
`isArtinian_iff` 📖	mathematical	—	`IsArtinian` `Submodule` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	—	`isWellFounded_iff`
`isArtinian_iff_submodule_quotient` 📖	mathematical	—	`IsArtinian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module` `HasQuotient.Quotient` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`isArtinian_submodule'` `isArtinian_of_quotient_of_artinian` `isArtinian_of_range_eq_ker` `RingHomSurjective.ids` `Submodule.ker_mkQ` `Submodule.range_subtype`
`isArtinian_of_fg_of_artinian` 📖	mathematical	`Submodule.FG` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`IsArtinian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_of_fg_of_artinian'` `Module.Finite.iff_fg`
`isArtinian_of_fg_of_artinian'` 📖	mathematical	—	`IsArtinian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	—	`Module.Finite.exists_fin'` `isArtinian_of_surjective` `isArtinian_pi'` `Finite.of_fintype`
`isArtinian_of_finite` 📖	mathematical	—	`IsArtinian`	—	`Finite.wellFounded_of_trans_of_irrefl` `SetLike.instFinite` `instIsTransLt` `instIrreflLt`
`isArtinian_of_injective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`IsArtinian`	—	`RingHomSurjective.ids` `Submodule.map_strictMono_of_injective` `IsWellFounded.wf`
`isArtinian_of_le` 📖	mathematical	`Submodule` `Preorder.toLE` `PartialOrder.toPreorder` `Submodule.instPartialOrder`	`IsArtinian` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_of_injective` `Submodule.inclusion_injective`
`isArtinian_of_linearEquiv` 📖	mathematical	—	`IsArtinian`	—	`RingHomInvPair.ids` `isArtinian_of_surjective` `Equiv.surjective`
`isArtinian_of_quotient_of_artinian` 📖	mathematical	—	`IsArtinian` `HasQuotient.Quotient` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `Submodule.hasQuotient` `Submodule.Quotient.addCommGroup` `Submodule.Quotient.module`	—	`isArtinian_of_surjective` `Submodule.Quotient.mk_surjective`
`isArtinian_of_range_eq_ker` 📖	mathematical	`LinearMap.range` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `LinearMap.ker`	`IsArtinian`	—	`RingHomSurjective.ids` `wellFounded_lt_exact_sequence` `Submodule.instIsModularLattice` `isArtinian_of_quotient_of_artinian` `isArtinian_submodule'` `le_rfl` `LinearMap.ker_eq_bot` `Submodule.ker_liftQ_eq_bot` `LinearMap.surjective_rangeRestrict` `Submodule.map_comap_eq` `Submodule.range_liftQ` `inf_comm` `Submodule.comap_map_eq` `LinearMap.ker_rangeRestrict`
`isArtinian_of_submodule_of_artinian` 📖	mathematical	—	`IsArtinian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_submodule'`
`isArtinian_of_surjective` 📖	mathematical	`DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike`	`IsArtinian`	—	`Submodule.comap_strictMono_of_surjective` `RingHomSurjective.ids` `IsWellFounded.wf`
`isArtinian_of_surjective_algebraMap` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap`	`IsArtinian`	—	`OrderEmbedding.wellFoundedLT` `Submodule.smul_mem` `Algebra.algebraMap_eq_smul_one` `smul_assoc` `one_smul` `Submodule.ext_iff`
`isArtinian_of_tower` 📖	mathematical	—	`IsArtinian`	—	`OrderEmbedding.wellFounded` `IsWellFounded.wf`
`isArtinian_pi` 📖	mathematical	`IsArtinian` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid`	`Pi.addCommMonoid` `Pi.module`	—	`Finite.induction_empty_option` `isArtinian_of_linearEquiv` `Finite.to_wellFoundedLT` `Finite.of_fintype` `Unique.instSubsingleton` `PEmpty.instIsEmpty` `RingHomInvPair.ids` `isArtinian_prod`
`isArtinian_pi'` 📖	mathematical	—	`IsArtinian` `Ring.toSemiring` `Pi.addCommMonoid` `AddCommGroup.toAddCommMonoid` `Pi.Function.module`	—	`isArtinian_pi`
`isArtinian_prod` 📖	mathematical	—	`IsArtinian` `Ring.toSemiring` `Prod.instAddCommMonoid` `AddCommGroup.toAddCommMonoid` `Prod.instModule`	—	`isArtinian_of_range_eq_ker` `LinearMap.range_inl`
`isArtinian_range` 📖	mathematical	—	`IsArtinian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `LinearMap.range` `RingHom.id` `Semiring.toNonAssocSemiring` `RingHomSurjective.ids` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_of_surjective` `RingHomSurjective.ids` `LinearMap.surjective_rangeRestrict`
`isArtinian_span_of_finite` 📖	mathematical	—	`IsArtinian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `Submodule.span` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_of_fg_of_artinian` `Submodule.fg_def`
`isArtinian_submodule'` 📖	mathematical	—	`IsArtinian` `Submodule` `SetLike.instMembership` `Submodule.setLike` `Submodule.addCommMonoid` `Submodule.module`	—	`isArtinian_of_injective` `Subtype.val_injective`
`isArtinian_sup` 📖	mathematical	—	`IsArtinian` `Submodule` `Ring.toSemiring` `AddCommGroup.toAddCommMonoid` `SetLike.instMembership` `Submodule.setLike` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `Submodule.completeLattice` `Submodule.addCommMonoid` `Submodule.module`	—	`RingHomSurjective.ids` `isArtinian_range` `isArtinian_prod` `Submodule.range_subtype` `LinearMap.range_coprod`
`monotone_stabilizes_iff_artinian` 📖	mathematical	—	`DFunLike.coe` `OrderHom` `OrderDual` `Submodule` `Nat.instPreorder` `OrderDual.instPreorder` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `OrderHom.instFunLike` `IsArtinian`	—	`wellFoundedGT_iff_monotone_chain_condition`
`set_has_minimal_iff_artinian` 📖	mathematical	—	`Submodule` `Set` `Set.instMembership` `Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `IsArtinian`	—	`isArtinian_iff` `WellFounded.wellFounded_iff_has_min`

---

← Back to Index