smul_of — Mathlib

English

For any g in G and any scalar r in k, the scalar action on the basis element corresponding to g equals the basis element at g with coefficient r: r • of k G g = single g r.

Русский

Для любого элемента g в G и скаляра r в k скалярное умножение на базисный элемент g даёт δ_g с коэффициентом r: r • of k G g = single g r.

LaTeX

$$$$r \cdot \text{of } k G g = \text{single } g\; r.$$$$

Lean4

theorem smul_of [MulOneClass G] (g : G) (r : k) : r • of k G g = single g r := by simp

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