Documentation

CompPoly.Univariate.ToPoly.Degree

`toPoly` Degree Lemmas #

Degree lemmas for the computable-univariate to Polynomial conversion.

theorem CompPoly.CPolynomial.toPoly_smul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (r : R) (p : CPolynomial R) :

(r • p).toPoly = r • p.toPoly

noncomputable def CompPoly.CPolynomial.toPolyLinearEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] :

CPolynomial R ≃ₗ[R] Polynomial R

Instances For

theorem CompPoly.CPolynomial.degree_le_iff_coeff_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : WithBot ℕ) :

p.degree ≤ n ↔ ∀ (k : ℕ), n < ↑k → p.coeff k = 0

theorem CompPoly.CPolynomial.degree_lt_iff_coeff_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) :

p.degree < ↑n ↔ ∀ (k : ℕ), n ≤ k → p.coeff k = 0

theorem CompPoly.CPolynomial.mem_degreeLE {R : Type u_1} [Semiring R] {n : WithBot ℕ} {p : CPolynomial R} :

p ∈ degreeLE n ↔ p.degree ≤ n

theorem CompPoly.CPolynomial.degreeLE_mono {R : Type u_1} [Semiring R] (m n : WithBot ℕ) (h_lessThan : m ≤ n) :

degreeLE m ≤ degreeLE n

theorem CompPoly.CPolynomial.mem_degreeLT {R : Type u_1} [Semiring R] {n : ℕ} {p : CPolynomial R} :

p ∈ degreeLT n ↔ p.degree < ↑n

theorem CompPoly.CPolynomial.degreeLT_mono {R : Type u_1} [Semiring R] {m n : ℕ} (h : m ≤ n) :

degreeLT m ≤ degreeLT n

theorem CompPoly.CPolynomial.degreeLT_succ_eq_degreeLE {R : Type u_1} [Semiring R] {n : ℕ} :

degreeLT (n + 1) = degreeLE ↑n

theorem CompPoly.CPolynomial.monomial_mem_degreeLT {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {n : ℕ} (i : Fin n) (c : R) :

monomial (↑i) c ∈ degreeLT n

theorem CompPoly.CPolynomial.degreeLTEquiv_invFun_mem {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (f : Fin n → R) :

∑ i : Fin n, monomial (↑i) (f i) ∈ degreeLT n

theorem CompPoly.CPolynomial.degreeLTEquiv_left_inv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (p : ↑(degreeLT n)) :

⟨∑ i : Fin n, monomial (↑i) ((↑p).coeff ↑i), ⋯⟩ = p

theorem CompPoly.CPolynomial.degreeLTEquiv_right_inv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) (f : Fin n → R) :

(fun (i : Fin n) => (∑ j : Fin n, monomial (↑j) (f j)).coeff ↑i) = f

def CompPoly.CPolynomial.degreeLTEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) :

↑(degreeLT n) ≃ₗ[R] Fin n → R

Instances For

@[reducible, inline]

abbrev CompPoly.CPolynomial.degreeLTLinearEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] (n : ℕ) :

↑(degreeLT n) ≃ₗ[R] Fin n → R

Instances For

theorem CompPoly.CPolynomial.degreeLTEquiv_toPoly {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {n : ℕ} {p : CPolynomial R} (hp : p ∈ degreeLT n) (i : Fin n) :

(degreeLTEquiv n) ⟨p, hp⟩ i = (Polynomial.degreeLTEquiv R n) ⟨p.toPoly, ⋯⟩ i

theorem CompPoly.CPolynomial.degreeLTEquiv_eq_zero_iff_eq_zero {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {n : ℕ} {p : CPolynomial R} (hp : p ∈ degreeLT n) :

(degreeLTEquiv n) ⟨p, hp⟩ = 0 ↔ p = 0

theorem CompPoly.CPolynomial.eval_eq_sum_degreeLTEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [DecidableEq R] {n : ℕ} {p : CPolynomial R} (hp : p ∈ degreeLT n) (x : R) :

eval x p = ∑ i : Fin n, (degreeLTEquiv n) ⟨p, hp⟩ i * x ^ ↑i