English
If q is monic of degree n and p*q is monic of degree m+n, then p is monic of degree m.
Русский
Если q мономичен степени n и p*q мономичен степени m+n, то p мономичен степени m.
LaTeX
$$$IsMonicOfDegree(q, n) \\land IsMonicOfDegree(p * q, m + n) \\Rightarrow IsMonicOfDegree(p, m)$$$
Lean4
theorem of_mul_right {p q : R[X]} {m n : ℕ} (hq : IsMonicOfDegree q n) (hpq : IsMonicOfDegree (p * q) (m + n)) :
IsMonicOfDegree p m := by
rcases subsingleton_or_nontrivial R with H | H
· simp only [isMonicOfDegree_iff_of_subsingleton, Nat.add_eq_zero] at hpq ⊢
exact hpq.1
have h₂ : p.Monic := hq.monic.of_mul_monic_right hpq.monic
refine ⟨?_, h₂⟩
have := hpq.natDegree_eq
have h : p.leadingCoeff * q.leadingCoeff ≠ 0 :=
by
rw [h₂.leadingCoeff, hq.leadingCoeff_eq, one_mul]
exact one_ne_zero
rw [natDegree_mul' h, hq.natDegree_eq] at this
exact (Nat.add_right_cancel this.symm).symm
