English
The weighted order of a product is at least the sum of the weighted orders.
Русский
Весовой порядок произведения не меньше суммы весовых порядков.
LaTeX
$$f.weightedOrder w + g.weightedOrder w ≤ (f*g).weightedOrder w$$
Lean4
/-- The weighted_order of the product of two formal power series
is at least the sum of their orders. -/
theorem le_weightedOrder_mul : f.weightedOrder w + g.weightedOrder w ≤ weightedOrder w (f * g) := by
classical
apply le_weightedOrder
intro d hd
rw [coeff_mul, Finset.sum_eq_zero]
rintro ⟨i, j⟩ hij
by_cases hi : weight w i < f.weightedOrder w
· rw [coeff_eq_zero_of_lt_weightedOrder w hi, zero_mul]
· by_cases hj : weight w j < g.weightedOrder w
· rw [coeff_eq_zero_of_lt_weightedOrder w hj, mul_zero]
· rw [not_lt] at hi hj
simp only [Finset.mem_antidiagonal] at hij
exfalso
apply ne_of_lt (lt_of_lt_of_le hd <| add_le_add hi hj)
rw [← hij, map_add, Nat.cast_add]
