degree_weierstrassMod_lt — Mathlib

English

If f,g are as above and n is the order of g modulo the residue field, then the degree of the remainder f %ʷ g is strictly less than n.

Русский

Если f и g удовлетворяют условиям выше, и n — порядок образа g в резидуальном поле, то deg( f %ʷ g ) < n.

LaTeX

$$$\deg(f\%\!\wp g) < n, \quad n = \operatorname{order}(g \bmod \mathfrak m)$$$

Lean4

theorem degree_weierstrassMod_lt [IsPrecomplete (IsLocalRing.maximalIdeal A) A] :
    (f %ʷ g).degree < (g.map (IsLocalRing.residue A)).order.toNat :=
  by
  rw [weierstrassMod]
  split_ifs with hg
  · exact degree_trunc_lt _ _
  · nontriviality A
    rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _

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