divMonomial — Mathlib

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

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