toFinsupp_zsmul — Mathlib

English

The same ℤ-action compatibility with the finsupp embedding holds in the stated form: toFinsupp(a • b) = a • toFinsupp(b).

Русский

Та же совместимость действия ℤ с вложением в Finsupp: toFinsupp(a • b) = a • toFinsupp(b).

LaTeX

$$$ (a : \mathbb{Z})\ (b : R[X]), (a \cdot b).toFinsupp = a \cdot b.toFinsupp$$$

Lean4

@[simp]
theorem toFinsupp_zsmul (a : ℤ) (b : R[X]) : (a • b).toFinsupp = a • b.toFinsupp :=
  rfl

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