mem_asIdeal — Mathlib

English

For any two-sided ideal I and any element x of the ring, x belongs to the associated left ideal I.asIdeal if and only if x belongs to I.

Русский

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

LaTeX

$$$x \in I.asIdeal \iff x \in I$$$

Lean4

@[simp]
theorem mem_asIdeal {I : TwoSidedIdeal R} {x : R} : x ∈ asIdeal I ↔ x ∈ I := by simp [asIdeal]

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