toPoly Equivalence

Ring equivalences between computable univariate polynomials and Polynomial.

theorem CompPoly.CPolynomial.Raw.toPoly_neg {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] (p : Raw R) : (-p).toPoly = -p.toPoly

theorem CompPoly.CPolynomial.toPoly_neg {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : (-p).toPoly = -p.toPoly

theorem CompPoly.CPolynomial.toPoly_add {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p + q).toPoly = p.toPoly + q.toPoly

theorem CompPoly.CPolynomial.Raw.toPoly_sub {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] (p q : Raw R) : (p - q).toPoly = p.toPoly - q.toPoly

theorem CompPoly.CPolynomial.toPoly_sub {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p - q).toPoly = p.toPoly - q.toPoly

theorem CompPoly.CPolynomial.Raw.toPoly_mul_coeff {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) (i : ℕ) : (p * q).toPoly.coeff i = (p.toPoly * q.toPoly).coeff i

theorem CompPoly.CPolynomial.Raw.toPoly_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : Raw R) : (p * q).toPoly = p.toPoly * q.toPoly

theorem CompPoly.CPolynomial.toPoly_mul_coeffC {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) (i : ℕ) : (↑p * ↑q).toPoly.coeff i = ((↑p).toPoly * (↑q).toPoly).coeff i

theorem CompPoly.CPolynomial.toPoly_mul {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p q : CPolynomial R) : (p * q).toPoly = p.toPoly * q.toPoly

@[simp]

theorem CompPoly.CPolynomial.eval₂_C {R : Type u_2} [Semiring R] {S : Type u_3} [Semiring S] (f : R →+* S) (x : S) (r : R) : Raw.eval₂ f x (Raw.C r) = f r

@[simp]

theorem CompPoly.CPolynomial.Raw.toPoly_C {R : Type u_2} [Semiring R] (r : R) : (C r).toPoly = Polynomial.C r

@[simp]

theorem CompPoly.CPolynomial.Raw.toPoly_one {R : Type u_2} [Semiring R] : toPoly 1 = 1

theorem CompPoly.CPolynomial.toPoly_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : toPoly 1 = 1

theorem CompPoly.CPolynomial.Raw.toPoly_pow {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] (p : Raw R) (n : ℕ) : (p ^ n).toPoly = p.toPoly ^ n

@[simp]

theorem CompPoly.CPolynomial.Raw.toPoly_zero {R : Type u_2} [Semiring R] : toPoly 0 = 0

theorem CompPoly.CPolynomial.toPoly_zero {R : Type u_2} [Semiring R] : toPoly 0 = 0

@[simp]

theorem CompPoly.CPolynomial.Raw.toPoly_X {R : Type u_2} [Semiring R] : X.toPoly = Polynomial.X

theorem CompPoly.CPolynomial.toPoly_pow {R : Type u_1} [Semiring R] [BEq R] [Nontrivial R] [LawfulBEq R] (p : CPolynomial R) (n : ℕ) : (p ^ n).toPoly = p.toPoly ^ n

theorem CompPoly.CPolynomial.toPoly_sum {R : Type u_2} [Semiring R] [BEq R] [LawfulBEq R] {ι : Type u} [DecidableEq ι] {s : Finset ι} {f : ι → CPolynomial R} : (∑ j ∈ s, f j).toPoly = ∑ j ∈ s, (f j).toPoly

theorem CompPoly.CPolynomial.toPoly_prod {R : Type u_2} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] {ι : Type u} [DecidableEq ι] {s : Finset ι} {f : ι → CPolynomial R} : (∏ j ∈ s, f j).toPoly = ∏ j ∈ s, (f j).toPoly

noncomputable def CompPoly.CPolynomial.ringEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CPolynomial R ≃+* Polynomial R

Equations

• CompPoly.CPolynomial.ringEquiv = { toFun := CompPoly.CPolynomial.toPoly, invFun := fun (p : Polynomial R) => ⟨p.toImpl, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem CompPoly.CPolynomial.ringEquiv_apply {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPolynomial R) : ringEquiv p = p.toPoly

The forward map of ringEquiv is toPoly.