English
Let P be a polynomial over a commutative semiring R. If every r ∈ R with r · P = 0 implies r = 0, and P · Q = 0 for some Q, then Q = 0.
Русский
Пусть P — полином над коммутативным полускольцом R. Если для любого r ∈ R верно r · P = 0 ⇒ r = 0, и существуют P · Q = 0, то Q = 0.
LaTeX
$$$ (\forall r \in R),\; r \cdot P = 0 \Rightarrow r = 0\ \land\ P \cdot Q = 0 \Rightarrow Q = 0 $$$
Lean4
theorem eq_zero_of_mul_eq_zero_of_smul (P : R[X]) (h : ∀ r : R, r • P = 0 → r = 0) (Q : R[X]) (hQ : P * Q = 0) :
Q = 0 :=
by
suffices ∀ i, P.coeff i • Q = 0 by
rw [← leadingCoeff_eq_zero]
apply h
simpa [ext_iff, mul_comm Q.leadingCoeff] using fun i ↦ congr_arg (·.coeff Q.natDegree) (this i)
apply Nat.strong_decreasing_induction
· use P.natDegree
intro i hi
rw [coeff_eq_zero_of_natDegree_lt hi, zero_smul]
intro l IH
obtain _ | hl := (natDegree_smul_le (P.coeff l) Q).lt_or_eq
· apply eq_zero_of_mul_eq_zero_of_smul _ h (P.coeff l • Q)
rw [smul_eq_C_mul, mul_left_comm, hQ, mul_zero]
suffices P.coeff l * Q.leadingCoeff = 0 by
rwa [← leadingCoeff_eq_zero, ← coeff_natDegree, coeff_smul, hl, coeff_natDegree, smul_eq_mul]
let m := Q.natDegree
suffices (P * Q).coeff (l + m) = P.coeff l * Q.leadingCoeff by rw [← this, hQ, coeff_zero]
rw [coeff_mul]
apply Finset.sum_eq_single (l, m) _ (by simp)
simp only [Finset.mem_antidiagonal, ne_eq, Prod.forall, Prod.mk.injEq, not_and]
intro i j hij H
obtain hi | rfl | hi := lt_trichotomy i l
· have hj : m < j := by omega
rw [coeff_eq_zero_of_natDegree_lt hj, mul_zero]
· cutsat
· rw [← coeff_C_mul, ← smul_eq_C_mul, IH _ hi, coeff_zero]
termination_by Q.natDegree
