English
Division by a monomial with coefficient 1 is defined by discarding terms not divisible by that monomial; the quotient is given by a standard division by monomial with exponent s.
Русский
Деление по мономиалу с коэффициентом 1 определяется как удаление всех членов полинома, не делимого на данный моном; частное по существующей схеме делится по степеням мономиала s.
LaTeX
$$$\\operatorname{divMonomial}(p,s) = p \\ /\\ Monomial(s)$$$
Lean4
/-- Divide by `monomial 1 s`, discarding terms not divisible by this. -/
noncomputable def divMonomial (p : MvPolynomial σ R) (s : σ →₀ ℕ) : MvPolynomial σ R :=
AddMonoidAlgebra.divOf p s