DetLow: the degree of the determinant of the agreement matrix in each variable

In each variable the determinant of the agreement matrix has degree at most the number of ones of g. This is a step of the proof of Lemma 3.6 of the paper.

theorem AaronsonAmbainis.DetLow.degreeOf_agMon_le {ι : Type} [Fintype ι] (x z : Cube ι) (j : ι) : MvPolynomial.degreeOf j (agMon x z) ≤ 1

Each entry of the agreement matrix has degree at most one in each variable.

theorem AaronsonAmbainis.DetLow.degreeOf_det_le {ι : Type} [Fintype ι] [DecidableEq ι] (g : Cube ι → Bool) (j : ι) : MvPolynomial.degreeOf j (agMatrix g).det ≤ Fintype.card (Ones g)

In the variable s_j the determinant of the agreement matrix has degree at most the number of ones of g (proof of Lemma 3.6 of the paper).