unop_eq_bot

Mathlib.Algebra.Ring.Subring.MulOpposite

URI: https://scilib.ai/kg/mathlib#Subring.unop_eq_bot

English

For subring S of R^op, S.unop = ⊥ iff S = ⊥.

Русский

Для подкольца S из R^op, S.unop = ⊥ тогда и только тогда S = ⊥.

LaTeX

$$$S^{unop} = \bot \iff S = \bot$$$

Lean4

@[simp]
theorem unop_eq_bot {S : Subring Rᵐᵒᵖ} : S.unop = ⊥ ↔ S = ⊥ :=
  unop_injective.eq_iff' unop_bot

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

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

Разделы

Аффилиация

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