unop_inj

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

Equality of unops implies equality of subsemirings.

Русский

Равенство не-предположений эквивалентно равенству подпsemiring.

LaTeX

$$$\forall {S T : \mathrm{Subsemiring}(R^{\mathrm{op}})}. S^{\mathrm{unop}} = T^{\mathrm{unop}} \Leftrightarrow S = T$$$

Lean4

@[simp]
theorem unop_inj {S T : Subsemiring Rᵐᵒᵖ} : S.unop = T.unop ↔ S = T :=
  opEquiv.symm.eq_iff_eq

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

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

Разделы

Аффилиация

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