Documentation Verification Report

Finiteness

📁 Source: Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean

Statistics

Metric	Count
Definitions `IsQuotientEquivQuotientPrime`	1
Theorems `mem_associatedPrimes_of_isFractionRing`, `bot_lt_annihilator_of_disjoint_nonZeroDivisors`, `nonempty_inter_nonZeroDivisors_of_faithfulSMul`, `exists_relSeries_isQuotientEquivQuotientPrime`, `induction_on_isQuotientEquivQuotientPrime`, `isQuotientEquivQuotientPrime_iff`, `finite`, `instFiniteMaximalSpectrumOfIsFractionRing`	8
Total	9

Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bot_lt_annihilator_of_disjoint_nonZeroDivisors` 📖	mathematical	`Disjoint` `Set` `OmegaCompletePartialOrder.toPartialOrder` `CompleteLattice.instOmegaCompletePartialOrder` `CompleteBooleanAlgebra.toCompleteLattice` `CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra` `Set.instCompleteAtomicBooleanAlgebra` `HeytingAlgebra.toOrderBot` `Order.Frame.toHeytingAlgebra` `CompleteDistribLattice.toFrame` `CompleteBooleanAlgebra.toCompleteDistribLattice` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors`	`Preorder.toLT` `PartialOrder.toPreorder` `Submodule.instPartialOrder` `Bot.bot` `Submodule.instBot` `Module.annihilator` `SetLike.instMembership` `Submodule.addCommMonoid` `Submodule.module`	—	`subset_union_prime_finite` `associatedPrimes.finite` `Module.Finite.self` `Disjoint.subset_compl_right` `biUnion_associatedPrimes_eq_compl_nonZeroDivisors` `SetLike.lt_iff_le_and_exists` `instIsConcreteLE` `bot_le` `Submodule.mem_annihilator` `mul_comm` `IsPrime.ne_top` `Set.instReflSubset`
`nonempty_inter_nonZeroDivisors_of_faithfulSMul` 📖	mathematical	—	`Set.Nonempty` `Set` `Set.instInter` `SetLike.coe` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Submodule.setLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule` `Submonoid` `MulZeroOneClass.toMulOneClass` `MonoidWithZero.toMulZeroOneClass` `Semiring.toMonoidWithZero` `Submonoid.instSetLike` `nonZeroDivisors`	—	`IsScalarTower.right` `LT.lt.ne'` `bot_lt_annihilator_of_disjoint_nonZeroDivisors` `Set.disjoint_iff_inter_eq_empty` `Module.annihilator_eq_bot`

Ideal.IsMaximal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_associatedPrimes_of_isFractionRing` 📖	mathematical	—	`Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set` `Set.instMembership` `associatedPrimes` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Semiring.toModule`	—	`associatedPrimes.finite` `Module.Finite.self` `Ideal.subset_union_prime_finite` `IsAssociatedPrime.isPrime` `Set.iUnion_congr_Prop` `biUnion_associatedPrimes_eq_compl_nonZeroDivisors` `ne_top` `Ideal.eq_top_of_isUnit_mem` `IsFractionRing.self_iff_nonZeroDivisors_le_isUnit` `eq_of_le` `Ideal.IsPrime.ne_top`

IsNoetherianRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_relSeries_isQuotientEquivQuotientPrime` 📖	mathematical	—	`RelSeries.head` `Submodule` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `setOf` `Submodule.IsQuotientEquivQuotientPrime` `Bot.bot` `Submodule.instBot` `RelSeries.last` `Top.top` `Submodule.instTop`	—	`WellFoundedGT.induction_top` `wellFoundedGT` `isNoetherian_of_isNoetherianRing_of_finite` `Submodule.Quotient.nontrivial_iff` `associatedPrimes.nonempty` `Submodule.mkQ_surjective` `Ideal.IsPrime.ne_top` `Set.instReflSubset` `Submodule.isQuotientEquivQuotientPrime_iff` `RelSeries.snoc.congr_simp` `RelSeries.last_snoc` `RelSeries.head_snoc`
`induction_on_isQuotientEquivQuotientPrime` 📖	—	—	—	—	`RingHomInvPair.ids` `Module.IsNoetherian.finite` `isNoetherian_of_isNoetherianRing_of_finite` `isNoetherian_of_finite` `Finite.of_fintype` `LinearEquiv.injective` `Function.surjective_to_subsingleton` `Zero.instNonempty` `LinearMap.exact_zero_iff_surjective` `LinearEquiv.surjective` `exists_relSeries_isQuotientEquivQuotientPrime` `isNoetherian_submodule'` `Unique.instSubsingleton` `add_lt_add_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `contravariant_swap_add_of_contravariant_add` `contravariant_lt_of_covariant_le` `RelSeries.step` `LT.lt.trans` `Module.Finite.quotient` `Submodule.injective_subtype` `Submodule.mkQ_surjective` `LinearMap.exact_subtype_mkQ`

Submodule

Definitions

Name	Category	Theorems
`IsQuotientEquivQuotientPrime` 📖	MathDef	2 math math: `IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime`, `isQuotientEquivQuotientPrime_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isQuotientEquivQuotientPrime_iff` 📖	mathematical	—	`IsQuotientEquivQuotientPrime` `Ideal.IsPrime` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `colon` `HasQuotient.Quotient` `Submodule` `AddCommGroup.toAddCommMonoid` `hasQuotient` `CommRing.toRing` `Quotient.addCommGroup` `Quotient.module` `Bot.bot` `instBot` `Ring.toSemiring` `Set` `Set.instSingletonSet` `DFunLike.coe` `LinearMap` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `mkQ` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `completeLattice` `span`	—	`le_rfl` `ker_liftQ_eq_bot` `ker_mkQ` `RingHomSurjective.ids` `range_liftQ` `LinearMap.range_comp` `map.congr_simp` `range_subtype` `mkQ_surjective` `Ideal.ext` `Ideal.instIsTwoSided_1` `SemilinearMapClass.toMulActionSemiHomClass` `LinearMap.semilinearMapClass` `SemilinearEquivClass.instSemilinearMapClass` `LinearEquiv.instSemilinearEquivClass` `Algebra.smul_def` `mul_one` `EquivLike.toEmbeddingLike` `AddMonoidHomClass.toZeroHomClass` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `SemilinearMapClass.distribMulActionSemiHomClass` `PrimeSpectrum.isPrime` `le_antisymm` `map_span` `Set.image_singleton` `Set.image_congr` `sup_comm` `comap_map_eq` `map_le_iff_le_comap` `Ideal.Quotient.span_singleton_one` `map_top` `LinearEquiv.range` `sup_le` `span_singleton_le_iff_mem` `LE.le.trans_eq` `le_sup_left` `le_sup_right` `mem_span_singleton_self` `instIsConcreteLE` `SMulMemClass.smul_mem` `smulMemClass` `RingHomInvPair.ids` `LinearMap.ker_eq_bot` `mapQ.eq_1` `LinearMap.range_eq_top` `LinearMap.range_toSpanSingleton` `LinearMap.submoduleOf_span_singleton_of_mem` `submoduleOf_sup_of_le` `submoduleOf_self`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteMaximalSpectrumOfIsFractionRing` 📖	mathematical	—	`Finite` `MaximalSpectrum` `CommRing.toCommSemiring`	—	`Equiv.finite_iff` `Set.finite_coe_iff` `Set.Finite.subset` `associatedPrimes.finite` `Module.Finite.self` `Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRing`

associatedPrimes

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`finite` 📖	mathematical	—	`Set.Finite` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `associatedPrimes` `AddCommGroup.toAddCommMonoid`	—	`IsNoetherianRing.induction_on_isQuotientEquivQuotientPrime` `eq_empty_of_subsingleton` `RingHomInvPair.ids` `eq_singleton_of_isPrimary` `Ideal.IsPrime.isPrimary` `PrimeSpectrum.isPrime` `LinearEquiv.AssociatedPrimes.eq` `Set.Finite.subset` `Set.Finite.union` `subset_union_of_exact`

---

← Back to Index