smul_modByMonic — Mathlib

English

Scalar multiplication commutes with taking a remainder modulo a monic polynomial: c · (p modₘ q) = (c · p) modₘ q.

Русский

Умножение на скаляр коммутирует с остатком по моному многочлену: c·(p modₘ q) = (c·p) modₘ q.

LaTeX

$$$$ c \\cdot (p \\bmod_{\\! m} q) = (c \\cdot p) \\bmod_{\\! m} q. $$$$

Lean4

theorem smul_modByMonic (c : R) (p : R[X]) : c • p %ₘ q = c • (p %ₘ q) :=
  by
  by_cases hq : q.Monic
  · rcases subsingleton_or_nontrivial R with hR | hR
    · simp only [eq_iff_true_of_subsingleton]
    ·
      exact
        (div_modByMonic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
            ⟨by rw [mul_smul_comm, ← smul_add, modByMonic_add_div p hq],
              (degree_smul_le _ _).trans_lt (degree_modByMonic_lt _ hq)⟩).2
  · simp_rw [modByMonic_eq_of_not_monic _ hq]

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