mul_assoc — Mathlib

English

Astute formal power series multiply associatively for mv power series: φ1 * φ2 * φ3 equals φ1 * (φ2 * φ3).

Русский

Множение многомерных формальных рядов ассоциативно: φ1 φ2 φ3 = φ1 (φ2 φ3).

LaTeX

$$$$ φ_1 * φ_2 * φ_3 = φ_1 * (φ_2 * φ_3) $$$$

Lean4

protected theorem mul_assoc (φ₁ φ₂ φ₃ : MvPowerSeries σ R) : φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃) :=
  by
  ext1 n
  classical
  simp only [coeff_mul, Finset.sum_mul, Finset.mul_sum, Finset.sum_sigma']
  apply
      Finset.sum_nbij' (fun ⟨⟨_i, j⟩, ⟨k, l⟩⟩ ↦ ⟨(k, l + j), (l, j)⟩) (fun ⟨⟨i, _j⟩, ⟨k, l⟩⟩ ↦ ⟨(i + k, l), (i, k)⟩) <;>
    aesop (add simp [add_assoc, mul_assoc])

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