isWeierstrassDivision_weierstrassDiv_weierstrassMod

English

If the residue ḡ ≠ 0, then there exist q,r with f = g q + r and r has degree < n; in particular f.IsWeierstrassDivision g q r holds for q = f /ʷ g and r = f %ʷ g.

Русский

Если образ ḡ не нулевой, то существуют q и r такие, что f = g q + r и deg r < n; в частности f.IsWeierstrassDivision g q r выполняется для q = f /ʷ g и r = f %ʷ g.

LaTeX

$$$\exists q \in A\llbracket X\rrbracket, \exists r \in A[X], \deg r < n : f = g q + r$ (при $n = \operatorname{ord}_{\bar A}(\bar g)$, $\bar g ≠ 0$)$$

Lean4

theorem isWeierstrassDivision_weierstrassDiv_weierstrassMod [IsAdicComplete (IsLocalRing.maximalIdeal A) A] :
    f.IsWeierstrassDivision g (f /ʷ g) (f %ʷ g) :=
  by
  simp_rw [weierstrassDiv, weierstrassMod, dif_pos hg]
  exact (IsWeierstrassDivisor.of_map_ne_zero hg).isWeierstrassDivisionAt_div_mod f

Похожие утверждения