English
If the residue of g is nonzero and g has a Weierstrass division g = q · (X^n) + r with deg r < n, then q is a unit.
Русский
Если образ g в остаточном поле не нулевой и g имеет деление Вейерштрасса g = q·X^n + r с deg r < n, то q является единицей.
LaTeX
$$$\pi(g) \neq 0$ and \exists q,r: g = q X^{n} + r, \ deg(r) < n \Rightarrow q \in A^\times$$$
Lean4
theorem isUnit_of_map_ne_zero {g q : A⟦X⟧} {r : A[X]} (hg : g.map (IsLocalRing.residue A) ≠ 0)
(H : (X ^ (g.map (IsLocalRing.residue A)).order.toNat).IsWeierstrassDivision g q r) : IsUnit q :=
by
obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H
set n := (g.map (IsLocalRing.residue A)).order.toNat
replace H2 := congr(coeff n (($H2).map (IsLocalRing.residue A)))
simp_rw [map_pow, map_X, coeff_X_pow_self, map_add, map_mul, coeff_map, Polynomial.coeff_coe,
Polynomial.coeff_eq_zero_of_degree_lt H1, map_zero, add_zero] at H2
rw [isUnit_iff_constantCoeff, ← isUnit_map_iff (IsLocalRing.residue A)]
rw [coeff_mul, ← Finset.sum_subset (s₁ := {(n, 0)}) (by simp) (fun p hp hnotMem ↦ ?_), Finset.sum_singleton,
coeff_map, coeff_map, coeff_zero_eq_constantCoeff, mul_comm] at H2
· exact isUnit_of_mul_eq_one _ _ H2.symm
· rw [coeff_of_lt_order p.1 ?_]
· rw [zero_mul]
· rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]
refine (Finset.antidiagonal.fst_le hp).lt_of_ne ?_
contrapose! hnotMem
rwa [Finset.mem_singleton, Finset.antidiagonal_congr hp (by simp)]
