ofFinsupp_smul — Mathlib

English

For a scalar a ∈ S acting on k via a SMulZeroClass, the scalar action commutes with the finsupp embedding: toFinsupp(a • b) = a • toFinsupp(b).

Русский

Для скаляра a ∈ S, действующего на k через SMulZeroClass, скалярное действие согласуется с вложением через finsupp: toFinsupp(a • b) = a • toFinsupp(b).

LaTeX

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

Lean4

@[simp]
theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S k] (a : S) (b : G →₀ k) :
    (⟨a • b⟩ : SkewMonoidAlgebra k G) = (a • ⟨b⟩ : SkewMonoidAlgebra k G) :=
  show _ = smul _ _ by rw [smul]

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