Documentation

CompPoly.Univariate.ToPoly.Equiv

toPoly Equivalence #

Ring equivalences between computable univariate polynomials and Polynomial.

source
theorem CompPoly.CPolynomial.toPoly_neg {R : Type u_2} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) :
(-p).toPoly = -p.toPoly
source
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
source
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
source
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
source
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
source
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
source
@[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
source
@[simp]
theorem CompPoly.CPolynomial.Raw.toPoly_C {R : Type u_2} [Semiring R] (r : R) :
(C r).toPoly = Polynomial.C r
source
@[simp]
theorem CompPoly.CPolynomial.Raw.toPoly_one {R : Type u_2} [Semiring R] :
toPoly 1 = 1
source
theorem CompPoly.CPolynomial.toPoly_one {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
toPoly 1 = 1
source
@[simp]
theorem CompPoly.CPolynomial.Raw.toPoly_zero {R : Type u_2} [Semiring R] :
toPoly 0 = 0
source
theorem CompPoly.CPolynomial.toPoly_zero {R : Type u_2} [Semiring R] :
toPoly 0 = 0
source
@[simp]
theorem CompPoly.CPolynomial.Raw.toPoly_X {R : Type u_2} [Semiring R] :
X.toPoly = Polynomial.X
source
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
source
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
source
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
source
noncomputable def CompPoly.CPolynomial.ringEquiv {R : Type u_1} [Semiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
CPolynomial R ≃+* Polynomial R
Instances For