mem_div_iff_of_nonzero — Mathlib

English

For nonzero J, x belongs to I/J if and only if for all y ∈ J, x·y ∈ I.

Русский

Для ненулевого J x ∈ I/J тогда и только тогда, когда для всех y ∈ J верно x y ∈ I.

LaTeX

$$$x \in I/J \iff \forall y \in J, x y \in I$$$

Lean4

theorem mem_div_iff_of_nonzero {I J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) {x} : x ∈ I / J ↔ ∀ y ∈ J, x * y ∈ I :=
  by
  rw [div_nonzero h]
  exact Submodule.mem_div_iff_forall_mul_mem

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