unop_op

Mathlib.Algebra.Ring.Subring.MulOpposite

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

English

The operation unop followed by op returns the original subring: (S.unop).op = S.

Русский

Операции unop, затем op возвращают исходное подкольцо: (S.unop).op = S.

LaTeX

$$$ (S^{\mathrm{unop}})^{\mathrm{op}} = S$$$

Lean4

@[simp]
theorem unop_op (S : Subring R) : S.op.unop = S :=
  rfl

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

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

Разделы

Аффилиация

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