mem_support_iff_exists_annihilator

English

A prime p lies in the support iff there exists m ∈ M with the annihilator of R m contained in p.

Русский

p принадлежит опоре тогда, когда существует m ∈ M, такой что аннигилятор модуля Rm включён в p.

LaTeX

$$$p \in \mathrm{Supp}_R(M) \iff \exists m \in M, (R \cdot m).\mathrm{annihilator} \le p.asIdeal$$$

Lean4

theorem mem_support_iff_exists_annihilator : p ∈ Module.support R M ↔ ∃ m : M, (R ∙ m).annihilator ≤ p.asIdeal :=
  by
  rw [Module.mem_support_iff']
  simp_rw [not_imp_not, SetLike.le_def, Submodule.mem_annihilator_span_singleton]

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