opRingEquiv_symm_single — Mathlib

English

The inverse opposite isomorphism sends a basis element back to the corresponding opposite basis element.

Русский

Обратный противоположный изоморфизм возвращает базисный элемент к соответствующему противоположному базисному элементу.

LaTeX

$$MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop)$$

Lean4

theorem opRingEquiv_symm_single [Mul G] (r : kᵐᵒᵖ) (x : Gᵐᵒᵖ) :
    MonoidAlgebra.opRingEquiv.symm (single x r) = op (single x.unop r.unop) := by simp

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