mod — Mathlib

English

The remainder r in the Weierstrass division is defined as mod f, i.e., r = (f − g · div f) truncated to degree n, where n is the order of g modulo I.

Русский

Остаток r в делении по Вейерштрассу определяется как mod f, то есть r = (f − g · div f), усечённый до степени n, где n — порядок g по отношению к I.

LaTeX

$$$ \\mathrm{mod} = (f - g \\cdot H.div f)_{\\le n-1}, \\; n = (g.map (Ideal.Quotient.mk I)).order.toNat. $$$

Lean4

/-- The remainder `r` in the proof of Weierstrass division. -/
noncomputable def mod [IsPrecomplete I A] : A[X] :=
  (f - g * H.div f).trunc (g.map (Ideal.Quotient.mk I)).order.toNat

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