self_mul_modByMonic — Mathlib

English

If q is monic, then the remainder of q * p upon division by q is zero: (q * p) %ₘ q = 0.

Русский

Если q мономический, то остаток от деления q p на q равен нулю: (q p) %ₘ q = 0.

LaTeX

$$$$ (q \\cdot p) %ₘ q = 0. $$$$

Lean4

/-- See `Polynomial.mul_self_modByMonic` for the other multiplication order. That version, unlike
this one, requires commutativity. -/
@[simp]
theorem self_mul_modByMonic (hq : q.Monic) : (q * p) %ₘ q = 0 :=
  by
  rw [modByMonic_eq_zero_iff_dvd hq]
  exact dvd_mul_right q p

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