modByMonic_zero — Mathlib

English

The remainder equals the original p minus q times the quotient: p %ₘ q = p − q · (p /ₘ q).

Русский

Остаток равен p минус q на частное: p %ₘ q = p − q · (p /ₘ q).

LaTeX

$$$ p \%_{m} q = p - q \cdot (p /_{m} q) $$$

Lean4

@[simp]
theorem modByMonic_zero (p : R[X]) : p %ₘ 0 = p :=
  letI := Classical.decEq R
  if h : Monic (0 : R[X]) then by
    haveI := monic_zero_iff_subsingleton.mp h
    simp [eq_iff_true_of_subsingleton]
  else by unfold modByMonic divModByMonicAux; rw [dif_neg h]

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