toFinsupp_smul — Mathlib

English

The scalar action on SkewMonoidAlgebra corresponds to the scalar action on finsupp: (a • b).toFinsupp = a • b.toFinsupp.

Русский

Скалярное действие на SkewMonoidAlgebra соответствует скалярному действию на finsupp: (a • b).toFinsupp = a • b.toFinsupp.

LaTeX

$$$ (a \cdot b).toFinsupp = a \cdot b^{\mathrm{toFinsupp}} $$$

Lean4

@[simp]
theorem toFinsupp_smul {S : Type*} [SMulZeroClass S k] (a : S) (b : SkewMonoidAlgebra k G) :
    (a • b).toFinsupp = a • b.toFinsupp := by rw [← ofFinsupp_smul]

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