English
Dividing by maximal X-power commutes with multiplication: divXPowOrder(f) · divXPowOrder(g) = divXPowOrder(f g).
Русский
Разделение на максимальную степень X сохраняет умножение: divXPowOrder(f) · divXPowOrder(g) = divXPowOrder(f g).
LaTeX
$$$ \\operatorname{divXPowOrder}(f) \\cdot \\operatorname{divXPowOrder}(g) = \\operatorname{divXPowOrder}(f \\cdot g) $$$
Lean4
/-- The operation of dividing a power series by the largest possible power of `X`
preserves multiplication. -/
theorem divXPowOrder_mul_divXPowOrder {f g : R⟦X⟧} : divXPowOrder f * divXPowOrder g = divXPowOrder (f * g) :=
by
by_cases h : f = 0 ∨ g = 0
· rcases h with (h | h) <;> simp [h]
push_neg at h
apply X_pow_mul_cancel (k := f.order.toNat + g.order.toNat)
calc
X ^ (f.order.toNat + g.order.toNat) * (f.divXPowOrder * g.divXPowOrder)
_ = (X ^ f.order.toNat * f.divXPowOrder) * (X ^ g.order.toNat * g.divXPowOrder) :=
by
conv_rhs => rw [mul_assoc, X_pow_mul, X_pow_mul, ← mul_assoc, mul_assoc, ← pow_add]
rw [X_pow_mul, add_comm]
_ = f * g := by simp [X_pow_order_mul_divXPowOrder]
_ = X ^ ((f * g).order.toNat) * (f * g).divXPowOrder := by simp [X_pow_order_mul_divXPowOrder]
_ = X ^ (f.order.toNat + g.order.toNat) * (f * g).divXPowOrder := by
rw [order_mul, ENat.toNat_add (order_eq_top.not.mpr h.1) (order_eq_top.not.mpr h.2)]
