mem_coeIdeal — Mathlib

English

For x ∈ P, x ∈ (I : FractionalIdeal S P) iff ∃ x' ∈ I with algebraMap x' = x.

Русский

Для x ∈ P верно: x принадлежит дробному идеалу I тогда и только тогда, когда существует x' ∈ I такое, что algebraMap x' = x.

LaTeX

$$x ∈ (I : FractionalIdeal S P) \leftrightarrow ∃ x' ∈ I, algebraMap R P x' = x$$

Lean4

@[simp]
theorem mem_coeIdeal {x : P} {I : Ideal R} : x ∈ (I : FractionalIdeal S P) ↔ ∃ x', x' ∈ I ∧ algebraMap R P x' = x :=
  mem_coeSubmodule _ _

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