ofFinsupp_nsmul — Mathlib

English

Let a be a natural number and b ∈ AddMonoidAlgebra R Nat. The polynomial corresponding to a • b is equal to a • (the polynomial corresponding to b).

Русский

Пусть a ∈ ℕ и b ∈ AddMonoidAlgebra R Nat. Полином, соответствующий a•b, равен a•(полином, соответствующий b).

LaTeX

$$$\\langle a \\cdot b \\rangle = a \\cdot \\langle b \\rangle$$$

Lean4

@[simp]
theorem ofFinsupp_nsmul (a : ℕ) (b) : (⟨a • b⟩ : R[X]) = (a • ⟨b⟩ : R[X]) :=
  rfl

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