mem_div_iff_forall_mul_mem

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.mem_div_iff_forall_mul_mem

English

Membership in I/J is equivalent to the property that x*y ∈ I for all y ∈ J.

Русский

Членство в I/J эквивалентно тому, что x*y ∈ I для каждого y ∈ J.

LaTeX

$$$x \in I/J \;\Leftrightarrow\; \forall y\in J,\; x*y \in I$$$

Lean4

theorem mem_div_iff_forall_mul_mem {x : A} {I J : Submodule R A} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I :=
  Iff.refl _

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

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

Разделы

Аффилиация

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