English
Let x be a Hahn series with coefficients in R and y a Hahn module element. The coefficient of x at the combined order x.order + y.order in the smoothed product equals the product of the leading coefficients: coeff((of R)^{-1}(x · y), x.order + y.order) = leadingCoeff(x) · leadingCoeff((of R)^{-1} y).
Русский
Пусть x — ряд Хана с коэффициентами в R, y — элемент модуля Хана. Коэффициент в суммарном порядке x.order + y.order в произведении равен произведению ведущих коэффициентов: coeff(..., x.order + y.order) = leadingCoeff(x) · leadingCoeff((of R)^{-1} y).
LaTeX
$$$\\displaystyle \\Big( (\\mathrm{of}\\, R)^{-1}(x \\cdot y) \\Big).\\mathrm{coeff}\\left( x.order + ((\\mathrm{of}\\, R).symm y).order \\right) = x.leadingCoeff \\cdot ((\\mathrm{of}\\, R).symm y).leadingCoeff.$$$
Lean4
theorem coeff_smul_order_add_order {Γ} [AddCommMonoid Γ] [LinearOrder Γ] [IsOrderedCancelAddMonoid Γ] [Zero R]
[SMulWithZero R V] (x : HahnSeries Γ R) (y : HahnModule Γ R V) :
((of R).symm (x • y)).coeff (x.order + ((of R).symm y).order) = x.leadingCoeff • ((of R).symm y).leadingCoeff :=
by
by_cases hx : x = (0 : HahnSeries Γ R); · simp [HahnSeries.coeff_zero, hx]
by_cases hy : (of R).symm y = 0; · simp [hy, coeff_smul]
rw [HahnSeries.order_of_ne hx, HahnSeries.order_of_ne hy, coeff_smul, HahnSeries.leadingCoeff_of_ne_zero hx,
HahnSeries.leadingCoeff_of_ne_zero hy, ← vadd_eq_add, Finset.vaddAntidiagonal_min_vadd_min, Finset.sum_singleton]
simp [HahnSeries.orderTop, hx, hy]
