Theorems · Theorem · commutative algebra

associatedPrimes.nonempty

∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_2) [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [IsNoetherianRing R] [Nontrivial M], (associatedPrimes R M).Nonempty

Defined in: Mathlib.RingTheory.Ideal.AssociatedPrime.Basic
Cited by: 4 results in Mathlib
Foundations: Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CommSemiring AddCommMonoid Module IsNoetherianRing Nontrivial

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites13

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Modulestatement and proof · cited by 20,661
AddCommMonoidstatement and proof · cited by 12,281
CommSemiringstatement and proof · cited by 10,911
Idealstatement and proof · cited by 4,748
Bot.botproof · cited by 4,720
Set.Nonemptystatement · cited by 2,627
Nontrivialstatement and proof · cited by 2,416
IsNoetherianRingstatement and proof · cited by 268
exists_neproof · cited by 101
Submodule.colonproof · cited by 80
associatedPrimesstatement · cited by 21
IsAssociatedPrimeproof · cited by 12

Cited by4

Results whose statement or proof uses this declaration.

IsSMulRegular.subsingleton_linearMap_iffproof · cited by 2
IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrimeproof · cited by 1
associatedPrimes.eq_singleton_of_isPrimaryproof · cited by 1
Module.associatedPrimes.minimalPrimes_annihilator_subset_associatedPrimesproof · cited by 0