mul_self_modByMonic — Mathlib

English

If q is monic, then (p·q) is 0 modulo q; i.e., (p·q) mod q = 0.

Русский

Если q моноик, то произведение p·q даёт нулевой остаток по модулю q.

LaTeX

$$$ (p \cdot q) \bmod q = 0 \quad \text{ if } q \text{ monic}. $$$

Lean4

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

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