English
Over a semiring with no zero divisors, p ∘ q = 0 if and only if either p = 0 or q is constant and p evaluated at that constant equals zero.
Русский
В полугруппе без нулевых делителей: p ∘ q = 0 тогда и только тогда, когда либо p = 0, либо q константа и p( q(0) ) = 0.
LaTeX
$$$p\\circ q = 0 \\iff p = 0 \\lor \\bigl(p( q(0) ) = 0 \\land q = C(q(0))\\bigr)$$$
Lean4
theorem comp_eq_zero_iff [Semiring R] [NoZeroDivisors R] {p q : R[X]} :
p.comp q = 0 ↔ p = 0 ∨ p.eval (q.coeff 0) = 0 ∧ q = C (q.coeff 0) :=
by
refine ⟨fun h ↦ ?_, Or.rec (fun h ↦ by simp [h]) fun h ↦ by rw [h.2, comp_C, h.1, C_0]⟩
have key : p.natDegree = 0 ∨ q.natDegree = 0 := by rw [← mul_eq_zero, ← natDegree_comp, h, natDegree_zero]
obtain key | key := Or.imp eq_C_of_natDegree_eq_zero eq_C_of_natDegree_eq_zero key
· rw [key, C_comp] at h
exact Or.inl (key.trans h)
· rw [key, comp_C, C_eq_zero] at h
exact Or.inr ⟨h, key⟩
