single_eq_algebraMap_mul_of — Mathlib

English

A basic decomposition: the basis element single a b decomposes as algebraMap k (SkewMonoidAlgebra k G) b times of k G a.

Русский

Базисный элемент single a b разлагается как algebraMap k (SkewMonoidAlgebra k G) b умноженное на of k G a.

LaTeX

$$$single\ a\ b = algebraMap k (SkewMonoidAlgebra k G) b \cdot of k G a$$$

Lean4

theorem single_eq_algebraMap_mul_of [MulSemiringAction G k] [SMulCommClass G k k] (a : G) (b : k) :
    single a b = algebraMap k (SkewMonoidAlgebra k G) b * of k G a := by
  simp [coe_algebraMap, comp_apply, of_apply, single_mul_single, one_mul, smul_one, mul_one]

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