English
If g has a Weierstrass factorization f h, then there exists a division of X^n by g giving a Weierstrass decomposition with f in one factor and the quotient in the other.
Русский
Если g имеет факторизацию Вейершстраса f h, то существует деление X^n деленного на g, приводящее к разложению Вейершстраc с f в одной части и с частиком в другой.
LaTeX
$$$\text{There exists } q,r \text{ with } (X^n) \mid_{W} g q r = g \;\text{and}\; g = (X^n) \cdot q + r, \ deg(r) < n$$$
Lean4
theorem isWeierstrassDivision {g : A⟦X⟧} {f : A[X]} {h : A⟦X⟧} (H : g.IsWeierstrassFactorization f h) :
(X ^ (g.map (IsLocalRing.residue A)).order.toNat).IsWeierstrassDivision g ↑H.isUnit.unit⁻¹
(Polynomial.X ^ (g.map (IsLocalRing.residue A)).order.toNat - f) :=
by
set n := (g.map (IsLocalRing.residue A)).order.toNat with hn
constructor
· refine (Polynomial.degree_sub_lt ?_ (Polynomial.monic_X_pow n).ne_zero ?_).trans_eq (by simpa)
· simp_rw [H.degree_eq_coe_lift_order_map, Polynomial.degree_X_pow, n, ENat.lift_eq_toNat_of_lt_top]
· rw [(Polynomial.monic_X_pow n).leadingCoeff, H.isDistinguishedAt.monic.leadingCoeff]
·
simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X,
add_sub_cancel]
