English
In a polynomial ring over a semiring, C r divides φ if and only if r divides every coefficient φ_i.
Русский
В полиномиальном кольце над полусемирингом C r делит φ тогда и только тогда, когда r делит каждый коэффициент φ_i.
LaTeX
$$$$C r \mid \varphi \quad\Longleftrightarrow\quad \forall i,\; r \mid \varphi_i$$$$
Lean4
theorem C_dvd_iff_dvd_coeff (r : R) (φ : R[X]) : C r ∣ φ ↔ ∀ i, r ∣ φ.coeff i :=
by
constructor
· rintro ⟨φ, rfl⟩ c
rw [coeff_C_mul]
apply dvd_mul_right
· intro h
choose c hc using h
classical
let c' : ℕ → R := fun i => if i ∈ φ.support then c i else 0
let ψ : R[X] := ∑ i ∈ φ.support, monomial i (c' i)
use ψ
ext i
simp only [c', ψ, coeff_C_mul, mem_support_iff, coeff_monomial, finset_sum_coeff, Finset.sum_ite_eq']
split_ifs with hi
· rw [hc]
· rw [Classical.not_not] at hi
rwa [mul_zero]
