English
Reduction modulo a polynomial b with unit leading coefficient is given by subtracting a suitable multiple of b from f to cancel its leading term, producing a new polynomial with smaller leading degree.
Русский
Редукция по полиному b с единицей ведущего коэффициента задаётся вычитанием подходящего множителя b из f, чтобы уничтожить его ведущий член, получив новое полиномиальное выражение с меньшей ведущей степенью.
LaTeX
$$$\\text{reduce}_{m}(hb, f) = f - \\operatorname{monomial}(\\deg_m f - \\deg_m b) (hb^{-1} \\cdot \\operatorname{lc}_m(f)) \\cdot b$$$
Lean4
/-- Reduce a polynomial modulo a polynomial with unit leading term (for some monomial order) -/
noncomputable def reduce {b : MvPolynomial σ R} (hb : IsUnit (m.leadingCoeff b)) (f : MvPolynomial σ R) :
MvPolynomial σ R :=
f - monomial (m.degree f - m.degree b) (hb.unit⁻¹ * m.leadingCoeff f) * b
