English
The lexicographic order on multivariate power series is defined by mapping a nonzero series to the least exponent among its support, using Lex on exponents; the zero series maps to the top element.
Русский
Лексикографический порядок на многовариантных рядах определяется по наименьшему показателю из поддержки ряда относительно порядка Lex; нулевой ряд отправляется в верхний элемент.
LaTeX
$$$\operatorname{lexOrder}: \mathrm{MvPowerSeries}(\sigma,R) \to \mathrm{WithTop}(\mathrm{Lex}(\sigma \to_0 \mathbb{N}))$$$
Lean4
theorem coeff_mul_of_add_lexOrder {φ ψ : MvPowerSeries σ R} {p q : σ →₀ ℕ} (hp : lexOrder φ = toLex p)
(hq : lexOrder ψ = toLex q) : coeff (p + q) (φ * ψ) = coeff p φ * coeff q ψ :=
by
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨p, q⟩ (by simp)]
rintro ⟨u, v⟩ h h'
simp only [Finset.mem_antidiagonal] at h
rcases trichotomy_of_add_eq_add (congrArg toLex h) with h'' | h'' | h''
· exact False.elim (h' (by simp [h''.1, h''.2]))
· rw [coeff_eq_zero_of_lt_lexOrder (d := u), zero_mul]
rw [hp]
norm_cast
· rw [coeff_eq_zero_of_lt_lexOrder (d := v), mul_zero]
rw [hq]
norm_cast
