English
For polynomials r with deg r less than the order, H.div r = 0.
Русский
Для полиномов r со степенью меньше порядка, H.div r = 0.
LaTeX
$$$ [IsAdicComplete I A] \\Rightarrow \\mathrm{div}(r) = 0 \\text{ when } \\deg(r) < n. $$$
Lean4
/-- The remainder map `PowerSeries.IsWeierstrassDivisorAt.mod` induces a linear map
`A⟦X⟧ / (g) →ₗ[A] A[X]`. -/
noncomputable def mod' [IsAdicComplete I A] : A⟦X⟧ ⧸ Ideal.span { g } →ₗ[A] A[X]
where
toFun :=
Quotient.lift (fun f ↦ H.mod f) fun f f' hf ↦
by
simp_rw [HasEquiv.Equiv, Submodule.quotientRel_def, Ideal.mem_span_singleton'] at hf
obtain ⟨a, ha⟩ := hf
obtain ⟨hf1, hf2⟩ := H.isWeierstrassDivisionAt_div_mod f
obtain ⟨hf'1, hf'2⟩ := H.isWeierstrassDivisionAt_div_mod f'
rw [eq_sub_iff_add_eq, hf2, hf'2, ← add_assoc, mul_comm, ← mul_add] at ha
exact (H.eq_of_mul_add_eq_mul_add hf'1 hf1 ha).2.symm
map_add' f
f' := by
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
obtain ⟨f', rfl⟩ := Ideal.Quotient.mk_surjective f'
exact H.mod_add f f'
map_smul' a
f := by
obtain ⟨f, rfl⟩ := Ideal.Quotient.mk_surjective f
exact H.mod_smul a f
