mem_asIdealOpposite — Mathlib

English

An element x of the opposite ring R^op lies in the image of I.asIdealOpposite if and only if its unop is in I.

Русский

Элемент x кольца-происхождения в R^op принадлежит образу I.asIdealOpposite тогда и только тогда, когда x.unop принадлежит I.

LaTeX

$$$x \in I.asIdealOpposite \iff x.unop \in I$$$

Lean4

theorem mem_asIdealOpposite {I : TwoSidedIdeal R} {x : Rᵐᵒᵖ} : x ∈ asIdealOpposite I ↔ x.unop ∈ I := by
  simpa [asIdealOpposite, asIdeal, TwoSidedIdeal.mem_iff, RingCon.op_iff] using ⟨I.ringCon.symm, I.ringCon.symm⟩

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