English
Over an integral domain, the order of the product of two formal power series equals the sum of their orders.
Русский
В интегрируемом $\,$домене порядок произведения двух формальных степенных рядов равен сумме их порядков.
LaTeX
$$$ \\operatorname{order}( \\phi \\cdot \\psi ) = \\operatorname{order}( \\phi ) + \\operatorname{order}( \\psi ) $$$
Lean4
/-- The order of the product of two formal power series over an integral domain
is the sum of their orders. -/
theorem order_mul (φ ψ : R⟦X⟧) : order (φ * ψ) = order φ + order ψ :=
by
apply le_antisymm _ (le_order_mul _ _)
by_cases h : φ = 0 ∨ ψ = 0
· rcases h with h | h <;> simp [h]
· push_neg at h
rw [← coe_toNat_order h.1, ← coe_toNat_order h.2, ← ENat.coe_add]
apply order_le
rw [coeff_mul, Finset.sum_eq_single_of_mem ⟨φ.order.toNat, ψ.order.toNat⟩ (by simp)]
· exact mul_ne_zero (coeff_order h.1) (coeff_order h.2)
· intro ij hij h
rcases trichotomy_of_add_eq_add (mem_antidiagonal.mp hij) with h' | h' | h'
· exact False.elim (h (by simp [Prod.ext_iff, h'.1, h'.2]))
· rw [coeff_of_lt_order_toNat ij.1 h', zero_mul]
· rw [coeff_of_lt_order_toNat ij.2 h', mul_zero]
