theorem Poly.mul_comm {q : ℕ} {n : ℕ} (a : R q n) (b : R q n) : a * b = b * a

theorem Poly.add_comm {q : ℕ} {n : ℕ} (a : R q n) (b : R q n) : a + b = b + a

@[simp]

theorem Poly.f_eq_zero {q : ℕ} {n : ℕ} : (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = 0

theorem Poly.mul_f_eq_zero {q : ℕ} {n : ℕ} (a : R q n) : a * (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = 0

theorem Poly.mul_one_eq {q : ℕ} {n : ℕ} (a : R q n) : 1 * a = a

theorem Poly.add_f_eq {q : ℕ} {n : ℕ} (a : R q n) : a + (Ideal.Quotient.mk (Ideal.span {f q n})) (f q n) = a

theorem Poly.add_zero_eq {a : ℕ} : a + 0 = a

theorem Poly.eq_iff_rep_eq {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) (b : R q n) : R.representative q n a = R.representative q n b ↔ a = b

theorem Poly.from_poly_zero {n : ℕ} {q : ℕ} : R.fromPoly 0 = 0

theorem Poly.rep_zero {q : ℕ} {n : ℕ} [Fact (q > 1)] : R.representative q n 0 = 0

theorem Poly.monomial_mul_mul {q : ℕ} {n : ℕ} (x : ℕ) (y : ℕ) : R.monomial 1 y * R.monomial 1 x = R.monomial 1 (x + y)

theorem R.toTensor_getD {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) (i : ℕ) : a.toTensor.getD i 0 = ZMod.toInt q (a.coeff i)

theorem R.toTensor_getD' {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (a : R q n) (i : ℕ) : ↑(a.toTensor.getD i 0) = a.coeff i

theorem R.monomial_zero_c_eq_zero {q : ℕ} {n : ℕ} {c : ℕ} : R.monomial 0 c = 0

theorem R.fromTensor_eq_concat_zero {q : ℕ} {n : ℕ} (tensor : List ℤ) : R.fromTensor tensor = R.fromTensor (tensor ++ [0])

theorem R.fromTensor_eq_concat_zeroes {q : ℕ} {n : ℕ} (tensor : List ℤ) (k : ℕ) : R.fromTensor (tensor ++ List.replicate k 0) = R.fromTensor tensor

@[simp]

theorem R.trimTensor_append_zero_eq (tensor : List ℤ) : trimTensor (tensor ++ [0]) = trimTensor tensor

@[simp]

theorem R.trimTensor_append_zeroes_eq (tensor : List ℤ) (n : ℕ) : trimTensor (tensor ++ List.replicate n 0) = trimTensor tensor

theorem R.trimTensor_append_not_zero (tensor : List ℤ) (x : ℤ) (hX : x ≠ 0) : trimTensor (tensor ++ [x]) = tensor ++ [x]

theorem R.trimTensor_eq_append_zeros (tensor : List ℤ) : ∃ (n : ℕ), tensor = trimTensor tensor ++ List.replicate n 0

theorem R.trimTensor_getD_0 {i : ℕ} (tensor : List ℤ) : tensor.getD i 0 = (trimTensor tensor).getD i 0

theorem R.trimTensor_trimTensor (tensor : List ℤ) : trimTensor (trimTensor tensor) = trimTensor tensor

theorem R.fromTensor_eq_fromTensor_trimTensor {q : ℕ} {n : ℕ} (tensor : List ℤ) : R.fromTensor (trimTensor tensor) = R.fromTensor tensor

theorem R.trimTensor_toTensor'_eq_trimTensor_toTensor {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) : trimTensor a.toTensor' = trimTensor a.toTensor

theorem Poly.eq_iff_coeff_eq {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (a : R q n) (b : R q n) : a = b ↔ (R.representative q n a).coeff = (R.representative q n b).coeff

theorem Poly.toTensor_length_eq_rep_length {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) : a.toTensor.length = a.repLength

theorem Poly.toTensor_length_eq_f_deg_plus_1 {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) : a.toTensor'.length = 2 ^ n + 1

theorem Poly.toTensor_trimTensor_eq_toTensor {q : ℕ} {n : ℕ} [Fact (q > 1)] (a : R q n) : trimTensor a.toTensor = a.toTensor

theorem Poly.R.trim_toTensor'_eq_toTensor {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (a : R q n) : trimTensor a.toTensor' = a.toTensor

theorem Poly.toTensor_fromTensor {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (tensor : List ℤ) (i : ℕ) (htensorlen : tensor.length < 2 ^ n) : (R.fromTensor tensor).toTensor.getD i 0 = tensor.getD i 0 % ↑q

theorem Poly.fromTensor_toTensor {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (a : R q n) (adeg : (R.representative q n a).natDegree + 1 < 2 ^ n) : R.fromTensor a.toTensor = a

theorem Poly.fromTensor_toTensor' {q : ℕ} {n : ℕ} [hqgt1 : Fact (q > 1)] (a : R q n) (adeg : (R.representative q n a).natDegree + 1 < 2 ^ n) : R.fromTensor a.toTensor' = a