noncomputable def HexPolyTheory.blockPolynomial (s : Hex.Matrix.Lists.Scaled) : Polynomial ℚ

A polynomial with integer coefficients and one common denominator.

Equations

• HexPolyTheory.blockPolynomial s = HexPolyTheory.polynomialOfList (HexMatrixTheory.decodeList s)

noncomputable def HexPolyTheory.integerPolynomial (xs : List ℤ) : Polynomial ℚ

Interpret integer coefficient lists in the rational polynomial ring.

Equations

• HexPolyTheory.integerPolynomial xs = HexPolyTheory.polynomialOfList (List.map (fun (z : ℚ) => z) do let a ← xs pure ↑a)

theorem HexPolyTheory.integerPolynomial_nil : integerPolynomial [] = 0

theorem HexPolyTheory.integerPolynomial_cons (x : ℤ) (xs : List ℤ) : integerPolynomial (x :: xs) = Polynomial.C ↑x + Polynomial.X * integerPolynomial xs

theorem HexPolyTheory.integerPolynomial_add (xs ys : List ℤ) : integerPolynomial (Hex.Matrix.Lists.add xs ys) = integerPolynomial xs + integerPolynomial ys

theorem HexPolyTheory.integerPolynomial_scale (a : ℤ) (xs : List ℤ) : integerPolynomial (Hex.Matrix.Lists.scale a xs) = Polynomial.C ↑a * integerPolynomial xs

theorem HexPolyTheory.integerPolynomial_mul (xs ys : List ℤ) : integerPolynomial (Hex.Matrix.Lists.mul xs ys) = integerPolynomial xs * integerPolynomial ys

theorem HexPolyTheory.blockPolynomial_scale (s : Hex.Matrix.Lists.Scaled) : blockPolynomial s = Polynomial.C (↑s.denom)⁻¹ * integerPolynomial s.nums

theorem HexPolyTheory.blockPolynomial_add (a b : Hex.Matrix.Lists.Scaled) (ha : 0 < a.denom) (hb : 0 < b.denom) : blockPolynomial (a.add b) = blockPolynomial a + blockPolynomial b

theorem HexPolyTheory.blockPolynomial_mul (a b : Hex.Matrix.Lists.Scaled) : blockPolynomial (a.mul b) = blockPolynomial a * blockPolynomial b

theorem HexPolyTheory.blockPolynomial_neg (a : Hex.Matrix.Lists.Scaled) : blockPolynomial a.neg = -blockPolynomial a

theorem HexPolyTheory.blockPolynomial_sub (a b : Hex.Matrix.Lists.Scaled) (ha : 0 < a.denom) (hb : 0 < b.denom) : blockPolynomial (a.sub b) = blockPolynomial a - blockPolynomial b

theorem HexPolyTheory.blockPolynomial_pow (a : Hex.Matrix.Lists.Scaled) (n : ℕ) : blockPolynomial (a.pow n) = blockPolynomial a ^ n

theorem HexPolyTheory.polynomialOfList_eq_block (xs : List ℚ) (a : Hex.Matrix.Lists.Scaled) (ha : 0 < a.denom) (h : Hex.Matrix.Lists.scaleRow a.denom xs a.nums = true) : polynomialOfList xs = blockPolynomial a

Cross products identify a rational coefficient list with a block.