associatedPrimes — Mathlib

English

The set of associated primes of a module M over R is the set of all prime ideals I that are associated to M.

Русский

Множество ассоциированных простых модулю M над R состоит из всех простых идеалов I, связанных с M.

LaTeX

$$$$\operatorname{associatedPrimes}(R,M) = \{ I \mid \IsAssociatedPrime I M\}. $$$$

Lean4

/-- The set of associated primes of a module. -/
def associatedPrimes : Set (Ideal R) :=
  {I | IsAssociatedPrime I M}

Похожие утверждения