English
If the ring is I-adically complete, then f is Weierstrass-divisible by g with quotient div f and remainder mod f, i.e., f = g · div f + mod f and deg(mod f) < n.
Русский
Если кольцо I-адически полное, то f делится на g по теореме Вейершстра: f = g·div f + mod f, причём deg(mod f) < n.
LaTeX
$$$ f = g \\cdot \\text{div} f + \\text{mod} f, \\quad \\deg(\\text{mod} f) < n, \\; n = \\operatorname{ord}((g \\mapsto \\mathrm{Quotient.mk} I))^\\text{toNat}. $$$
Lean4
/-- If the ring is `I`-adic complete, then `g` can be used as a divisor in Weierstrass division. -/
theorem isWeierstrassDivisionAt_div_mod [IsAdicComplete I A] : f.IsWeierstrassDivisionAt g (H.div f) (H.mod f) I :=
by
rcases eq_or_ne I ⊤ with rfl | hI
· have := ‹IsAdicComplete ⊤ A›.toIsHausdorff.subsingleton
rw [Subsingleton.elim f 0, Subsingleton.elim (H.div 0) 0, Subsingleton.elim (H.mod 0) 0]
exact g.isWeierstrassDivisionAt_zero _
constructor
· exact degree_trunc_lt _ _
· rw [mod, add_comm, ← sub_eq_iff_eq_add]
ext i
rw [Polynomial.coeff_coe, coeff_trunc]
split_ifs with hi
· rfl
refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
rw [SModEq.zero, smul_eq_mul, Ideal.mul_top,
show f - g * H.div f = f - g * (H.seq f k) - g * (H.div f - (H.seq f k)) by ring, map_sub]
exact
Ideal.sub_mem _ (H.coeff_seq_mem f k (not_lt.1 hi)) <|
coeff_mul_mem_ideal_of_coeff_right_mem_ideal' (H.coeff_div_sub_seq_mem f k) i
