opRingEquiv_op_X

Mathlib.RingTheory.Polynomial.Opposites

URI: https://scilib.ai/kg/mathlib#Polynomial.opRingEquiv_op_X

English

The opposite-ring isomorphism sends the variable X to X.

Русский

Противоположный кольцевой изоморфизм отправляет X в X.

LaTeX

$$$\operatorname{opRingEquiv}(R)(\operatorname{op}(X)) = X$$$

Lean4

@[simp]
theorem opRingEquiv_op_X : opRingEquiv R (op (X : R[X])) = X :=
  opRingEquiv_op_monomial 1 1

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

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

Разделы

Аффилиация

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