opRingEquiv_symm_monomial — Mathlib

English

The inverse of the opposite-ring isomorphism sends monomial n with coefficient r to op(monomial n (unop r)).

Русский

Обратное отображение противоположного кольца отправляет мономиал n с коэффициентом r в op(monomial n (unop r)).

LaTeX

$$$(\operatorname{opRingEquiv}(R)).{\text{symm}}(\operatorname{monomial} n r) = \operatorname{op}(\operatorname{monomial} n (\operatorname{unop} r))$$$

Lean4

@[simp]
theorem opRingEquiv_symm_monomial (n : ℕ) (r : Rᵐᵒᵖ) : (opRingEquiv R).symm (monomial n r) = op (monomial n (unop r)) :=
  (opRingEquiv R).injective (by simp)

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