Polynomials whose coefficients generate the unit ideal

If some combination ∑ i ∈ s, p.coeff (m i) * c i of coefficients of a multivariate polynomial p equals 1, then scalar multiplication on p is faithful: r • p = 0 forces r = 0. This holds in every commutative ring, including rings with torsion, where p having a nonzero coefficient would not be enough.

Main results

• MvPolynomial.eq_zero_of_smul_eq_zero_of_sum_coeff_mul_eq_one: if a combination of the coefficients of p is 1, then r • p = 0 forces r = 0.

theorem MvPolynomial.eq_zero_of_smul_eq_zero_of_sum_coeff_mul_eq_one {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] {p : MvPolynomial σ R} (s : Finset ι) (m : ι → σ →₀ ℕ) (c : ι → R) (hc : ∑ i ∈ s, p.coeff (m i) * c i = 1) {r : R} (h : r • p = 0) : r = 0

If some combination ∑ i ∈ s, p.coeff (m i) * c i of coefficients of p is 1, then r • p = 0 forces r = 0.