DetLow: multiplication by a polynomial with constant coefficient 1

Multiplying by a polynomial with constant coefficient 1 does not change the monomials of least total degree. This is Lemma 3.3 of the paper.

theorem AaronsonAmbainis.DetLow.coeff_unit_mul {ι : Type} [Fintype ι] (u q : MvPolynomial ι ℤ) (hu : MvPolynomial.constantCoeff u = 1) (m : ι →₀ ℕ) (hm : ∀ m' ∈ q.support, ∑ i : ι, m i ≤ ∑ i : ι, m' i) : (u * q).coeff m = q.coeff m

Key computation: if every monomial of q has total degree at least that of m, then u * q and q have the same coefficient at m (when u has constant coefficient 1).

theorem AaronsonAmbainis.DetLow.isLowest_unit_mul {ι : Type} [Fintype ι] (u q : MvPolynomial ι ℤ) (hu : MvPolynomial.constantCoeff u = 1) (m : ι →₀ ℕ) (h : IsLowest q m) : IsLowest (u * q) m

Forward direction of LowestUnit.

theorem AaronsonAmbainis.DetLow.exists_isLowest {ι : Type} [Fintype ι] (q : MvPolynomial ι ℤ) (hq : q ≠ 0) : ∃ (m : ι →₀ ℕ), IsLowest q m

A nonzero polynomial has a monomial of least total degree.

theorem AaronsonAmbainis.DetLow.isLowest_of_unit_mul {ι : Type} [Fintype ι] (u q : MvPolynomial ι ℤ) (hu : MvPolynomial.constantCoeff u = 1) (m : ι →₀ ℕ) (h : IsLowest (u * q) m) : IsLowest q m

Backward direction of LowestUnit.