mem_support_iff' — Mathlib

English

A prime p belongs to the support iff there exists m in M such that for all r not in p, r m ≠ 0.

Русский

Применимо: p ∈ Supp(M) эквивалентно существованию элемента m ∈ M, для которого ∀ r ∉ p, r m ≠ 0.

LaTeX

$$$p \in \mathrm{Supp}_R(M) \iff \exists m \in M, \forall r \notin p,\; r \cdot m \neq 0$$$

Lean4

theorem mem_support_iff' : p ∈ Module.support R M ↔ ∃ m : M, ∀ r ∉ p.asIdeal, r • m ≠ 0 :=
  by
  rw [← @not_not (_ ∈ _), notMem_support_iff']
  push_neg
  rfl

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