ofFinsupp_smul — Mathlib

English

For any S with a SMulZeroClass action on R, and a ∈ S, b ∈ R[X], the scalar action commutes with the finsupp embedding: (a • b).toFinsupp = a • (b.toFinsupp).

Русский

Для любого S с действием SMulZeroClass на R и для a ∈ S, b ∈ R[X], действие скаляра сохраняется через отображение toFinsupp: (a • b).toFinsupp = a • (b.toFinsupp).

LaTeX

$$$(a \\cdot b)^{\\wedge} = a \\cdot b^{\\wedge}$$$

Lean4

@[simp]
theorem ofFinsupp_smul {S : Type*} [SMulZeroClass S R] (a : S) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
  rfl

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