English
A scalar C r divides a polynomial φ if and only if r divides every coefficient of φ.
Русский
Число-скаля r делит полином φ тогда и только тогда, когда r делит каждый коэффициент φ.
LaTeX
$$$C r \\mid \\varphi \\;\\iff\\; \\forall i, r \\mid \\varphi_i$$$
Lean4
theorem C_dvd_iff_dvd_coeff (r : R) (φ : MvPolynomial σ R) : 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 ψ : MvPolynomial σ R := ∑ i ∈ φ.support, monomial i (c' i)
use ψ
apply MvPolynomial.ext
intro i
simp only [ψ, c', coeff_C_mul, coeff_sum, coeff_monomial, Finset.sum_ite_eq']
split_ifs with hi
· rw [hc]
· rw [notMem_support_iff] at hi
rwa [mul_zero]
