Theorems · Theorem · commutative algebra
associatedPrimes.finite
∀ (A : Type u) [inst : CommRing A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] [IsNoetherianRing A] [Module.Finite A M], (associatedPrimes A M).Finite
There are only finitely many associated primes of a finitely generated module over a Noetherian ring.
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 94 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites25
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- DFunLike.coeproof · cited by 62,936
- Modulestatement and proof · cited by 20,661
- RingHom.idproof · cited by 18,349
- CommRingstatement and proof · cited by 17,173
- AddCommGroupstatement and proof · cited by 12,871
- LinearMapproof · cited by 10,215
- Idealstatement · cited by 4,748
- LinearEquivproof · cited by 3,317
- HasQuotient.Quotientproof · cited by 2,301
- Set.Finitestatement and proof · cited by 1,814
- Module.Finitestatement and proof · cited by 1,032
- PrimeSpectrumproof · cited by 625
Cited by3
Results whose statement or proof uses this declaration.
- IsSMulRegular.subsingleton_linearMap_iffproof · cited by 2
- Ideal.bot_lt_annihilator_of_disjoint_nonZeroDivisorsproof · cited by 1
- Ideal.IsMaximal.mem_associatedPrimes_of_isFractionRingproof · cited by 0