modByMonic_eq_mod — Mathlib

English

If q is monic, then the mod by q equals the mod by the monic version of q. That is, p %ₘ q = p % q whenever q is monic.

Русский

Если q монический, то остаток от деления p на q равен остатку от деления p на моническое q. Иными словами, p %ₘ q = p % q, если q монический.

LaTeX

$$$ p \%_{\mathrm{monic}}\; q = p \%\; q \quad \text{если } q \text{ монический}$$$

Lean4

theorem modByMonic_eq_mod (p : R[X]) (hq : Monic q) : p %ₘ q = p % q :=
  show p %ₘ q = p %ₘ (q * C (leadingCoeff q)⁻¹) by simp only [Monic.def.1 hq, inv_one, mul_one, C_1]

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