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