op_inj

Mathlib.Algebra.Ring.Subsemiring.MulOpposite

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

English

Equality of opposites implies equality of subsemirings.

Русский

Равенство противоположных подпsemiring эквивалентно равенству самих подпsemiring.

LaTeX

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

Lean4

@[simp]
theorem op_inj {S T : Subsemiring R} : S.op = T.op ↔ S = T :=
  opEquiv.eq_iff_eq

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

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

Разделы

Аффилиация

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