mem_toTwoSided — Mathlib

English

For any two-sided ideal I, an element x lies in the two-sided version I.toTwoSided exactly when x lies in I.

Русский

Для любого двусторонного идеала I элемент x принадлежит I.toTwoSided тогда и только тогда, когда x принадлежит I.

LaTeX

$$$\forall x:\, x \in I.toTwoSided \iff x \in I$$$

Lean4

@[simp]
theorem mem_toTwoSided {I : Ideal R} [I.IsTwoSided] {x : R} : x ∈ I.toTwoSided ↔ x ∈ I := by simp [toTwoSided]

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