IsAssociatedPrime — Mathlib

English

An ideal I ⊆ R is an associated prime of a module M if I is prime and equals the annihilator of some element x ∈ M, i.e., I = ker(toSpanSingleton_R M x).

Русский

Идеал I ⊆ R является ассоциированной простой модуля M, если I — прост и равен аннилятору некоторого элемента x ∈ M, т.е. I = ker(toSpanSingleton_R M x).

LaTeX

$$$$\IsAssociatedPrime I M \iff I \text{ is prime and } \exists x:\, M,\ I = \ker(\text{toSpanSingleton } R M x). $$$$

Lean4

/-- `IsAssociatedPrime I M` if the prime ideal `I` is the annihilator of some `x : M`. -/
def IsAssociatedPrime : Prop :=
  I.IsPrime ∧ ∃ x : M, I = ker (toSpanSingleton R M x)

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