mem_iff

Mathlib.RingTheory.Ideal.AssociatedPrime.Basic

URI: https://scilib.ai/kg/mathlib#AssociatePrimes.mem_iff

English

Membership of I in associatedPrimes(R,M) is equivalent to I being IsAssociatedPrime I M.

Русский

Членство I в associatedPrimes(R,M) эквивалентно тому, что I является IsAssociatedPrime I M.

LaTeX

$$$$ I \in \operatorname{associatedPrimes}(R,M) \iff \IsAssociatedPrime I M. $$$$

Lean4

theorem mem_iff : I ∈ associatedPrimes R M ↔ IsAssociatedPrime I M :=
  Iff.rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru