mem_unop_iff

Mathlib.RingTheory.TwoSidedIdeal.Basic

URI: https://scilib.ai/kg/mathlib#TwoSidedIdeal.mem_unop_iff

English

For any I in Rᵐᵒᵖ, x ∈ I.unop iff op x ∈ I.

Русский

Для любого I в R^{op}, x ∈ I.unop ⇔ op x ∈ I.

LaTeX

$$x \in I.unop \iff op\,x \in I$$

Lean4

@[simp]
theorem mem_unop_iff {I : TwoSidedIdeal Rᵐᵒᵖ} {x : R} : x ∈ I.unop ↔ MulOpposite.op x ∈ I :=
  I.ringCon.comm'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru