opRingEquiv_single — Mathlib

English

For an additive monoid G, the opRingEquiv takes a basis element to the opposite-basis with r on the coefficient.

Русский

Для аддитивного моноида G, опRingEquiv переводит базисный элемент в противоположный базис с коэффициентом r.

LaTeX

$$AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r)$$

Lean4

theorem opRingEquiv_single [AddCommMagma G] (r : k) (x : G) :
    AddMonoidAlgebra.opRingEquiv (op (single x r)) = single x (op r) := by simp

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