English
If g · q = r with deg r < n for some power series q and polynomial r, then q = 0 and r = 0.
Русский
Если g · q = r при q — степенной ряд и r — многочлен с deg r < n, то q = 0 и r = 0.
LaTeX
$$$ g \\cdot q = r, \\; \\deg(r) < n \\; \\Rightarrow \\; q = 0 \\land r = 0. $$$
Lean4
/-- If `g * q = r` for some power series `q` and some polynomial `r` whose degree is `< n`,
then `q` and `r` are all zero. This implies the uniqueness of Weierstrass division. -/
theorem eq_zero_of_mul_eq [IsHausdorff I A] {q : A⟦X⟧} {r : A[X]}
(hdeg : r.degree < (g.map (Ideal.Quotient.mk I)).order.toNat) (heq : g * q = r) : q = 0 ∧ r = 0 :=
by
suffices ∀ k i, coeff i q ∈ I ^ k
by
have hq : q = 0 := by
ext i
refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
exact this _ _
rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq
exact ⟨hq, heq⟩
intro k
induction k with
| zero => simp
| succ k ih =>
rw [g.eq_X_pow_mul_shift_add_trunc (g.map (Ideal.Quotient.mk I)).order.toNat] at heq
have h1 : ∀ i, coeff i r ∈ I ^ (k + 1) := fun i ↦
by
rcases lt_or_ge i (g.map (Ideal.Quotient.mk I)).order.toNat with hi | hi
· rw [← heq, pow_succ']
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal i (fun j hj ↦ ?_) (fun j _ ↦ ih j) i le_rfl
rw [map_add, Polynomial.coeff_coe]
refine Ideal.add_mem _ ?_ (g.coeff_trunc_order_mem I j)
simp_rw [coeff_X_pow_mul', if_neg (lt_of_le_of_lt hj hi).not_ge, zero_mem]
simp_rw [Polynomial.coeff_coe, Polynomial.coeff_eq_zero_of_degree_lt (lt_of_lt_of_le hdeg (by simpa)), zero_mem]
rw [add_mul, mul_comm (X ^ _), ← eq_sub_iff_add_eq] at heq
replace heq := congr(H.isUnit_shift.unit⁻¹ * $heq)
rw [← mul_assoc, ← mul_assoc, IsUnit.val_inv_mul, one_mul] at heq
intro i
rw [← coeff_X_pow_mul _ (g.map (Ideal.Quotient.mk I)).order.toNat i, heq]
refine coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (fun i ↦ ?_) _
rw [map_sub]
refine Ideal.sub_mem _ (h1 _) ?_
rw [pow_succ']
refine coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (fun i ↦ ?_) ih _
simp_rw [Polynomial.coeff_coe, g.coeff_trunc_order_mem]
