unop_eq_bot

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

For a subsemiring S of Rᵐᵒᵖ, S.unop equals bottom if and only if S equals bottom.

Русский

Для подпол semiring S в Rᵐᵒᵖ, S.unop = ⊥ тогда и только тогда S = ⊥.

LaTeX

$$$S^{\\mathrm{unop}} = \\perp \\\\Longleftrightarrow S = \\perp$$$

Lean4

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

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

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

Разделы

Аффилиация

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