English
Nonzero leading coefficients ensure that the order of the product is the sum of the orders.
Русский
Ненулевые ведущие коэффициенты гарантируют, что порядок произведения равен сумме порядков.
LaTeX
$$$ (x*y).order = x.order + y.order \quad\text{if } x.leadingCoeff \neq 0 \land y.leadingCoeff \neq 0 $$$
Lean4
theorem order_mul_of_nonzero {x y : HahnSeries Γ R} (h : x.leadingCoeff * y.leadingCoeff ≠ 0) :
(x * y).order = x.order + y.order :=
by
have hx : x.leadingCoeff ≠ 0 := by aesop
have hy : y.leadingCoeff ≠ 0 := by aesop
have hxy : (x * y).coeff (x.order + y.order) ≠ 0 := ne_of_eq_of_ne (coeff_mul_order_add_order x y) h
refine
le_antisymm (order_le_of_coeff_ne_zero (Eq.mpr (congrArg (fun _a ↦ _a ≠ 0) (coeff_mul_order_add_order x y)) h)) ?_
rw [order_of_ne <| leadingCoeff_ne_zero.mp hx, order_of_ne <| leadingCoeff_ne_zero.mp hy,
order_of_ne <| ne_zero_of_coeff_ne_zero hxy, ← Set.IsWF.min_add]
exact Set.IsWF.min_le_min_of_subset support_mul_subset_add_support
