English
For a finite set of indices, the sum of the orders is not greater than the order of the product of the corresponding power series.
Русский
Для конечного множества индексов сумма порядков не превосходит порядок произведения соответствующих степенных рядов.
LaTeX
$$$\sum_{i \in s} \operatorname{order}(\phi_i) \le \operatorname{order}\Big(\prod_{i \in s} \phi_i\Big)$$$
Lean4
/-- The order of the product of two formal power series
is at least the sum of their orders. -/
theorem le_order_mul (φ ψ : R⟦X⟧) : order φ + order ψ ≤ order (φ * ψ) :=
by
apply le_order
intro n hn; rw [coeff_mul, Finset.sum_eq_zero]
rintro ⟨i, j⟩ hij
by_cases hi : ↑i < order φ
· rw [coeff_of_lt_order i hi, zero_mul]
by_cases hj : ↑j < order ψ
· rw [coeff_of_lt_order j hj, mul_zero]
rw [not_lt] at hi hj; rw [mem_antidiagonal] at hij
exfalso
apply ne_of_lt (lt_of_lt_of_le hn <| add_le_add hi hj)
rw [← Nat.cast_add, hij]
