single_eq_algebraMap_mul_of — Mathlib

English

The basis element corresponding to an element a of G with coefficient b equals the product of the scalar embedding of b and the basis element a.

Русский

Базисный элемент, соответствующий элементу a группы G с коэффициентом b, равен произведению векторной вставки b на базисный элемент a.

LaTeX

$$single a b = algebraMap k (MonoidAlgebra k G) b * of k G a$$

Lean4

theorem single_eq_algebraMap_mul_of [CommSemiring k] [Monoid G] (a : G) (b : k) :
    single a b = algebraMap k (MonoidAlgebra k G) b * of k G a := by simp

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