divByMonic_zero — Mathlib

English

If q is monic and deg q ≤ deg p, then deg q + deg(p /ₘ q) = deg p.

Русский

Если q монический и deg q ≤ deg p, то deg q + deg(p /ₘ q) = deg p.

LaTeX

$$$ \deg q + \deg(p /_{m} q) = \deg p \quad(\operatorname{Monic}(q),\ \deg q \le \deg p) $$$

Lean4

@[simp]
theorem divByMonic_zero (p : R[X]) : p /ₘ 0 = 0 :=
  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 divByMonic divModByMonicAux; rw [dif_neg h]

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