English
The product of a monomial and a general mv power series has coefficients given by a shifted multiplication with the coefficient a.
Русский
Произведение мономиала и общего mv-рядa даёт коэффициенты, сдвинутые на индекс мономиала и умножение на коэффициент a.
LaTeX
$$$$ \\operatorname{coeff}_{m}(\\operatorname{monomial}(n,a) \\cdot \phi) = \begin{cases} a \\cdot \\operatorname{coeff}_{m-n} \\phi, & n \\le m \\ 0, & \\text{otherwise} \\end{cases} $$$$
Lean4
theorem monomial_mul_monomial (m n : σ →₀ ℕ) (a b : R) : monomial m a * monomial n b = monomial (m + n) (a * b) := by
classical
ext k
simp only [coeff_mul_monomial, coeff_monomial]
split_ifs with h₁ h₂ h₃ h₃ h₂ <;> try rfl
· rw [← h₂, tsub_add_cancel_of_le h₁] at h₃
exact (h₃ rfl).elim
· rw [h₃, add_tsub_cancel_right] at h₂
exact (h₂ rfl).elim
· exact zero_mul b
· rw [h₂] at h₁
exact (h₁ <| le_add_left le_rfl).elim
