opRingEquiv_symm_C

Mathlib.RingTheory.Polynomial.Opposites

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

English

The inverse maps Cr to op(C(unop a)).

Русский

Обратное отображение переводит Cr к op(C(unop a)).

LaTeX

$$$(\operatorname{opRingEquiv}(R)).{\text{symm}}(C a) = C(\operatorname{op} (\operatorname{unop} a))$$$

Lean4

@[simp]
theorem opRingEquiv_symm_C (a : Rᵐᵒᵖ) : (opRingEquiv R).symm (C a) = op (C (unop a)) :=
  opRingEquiv_symm_monomial 0 a

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

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

Разделы

Аффилиация

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