Equivalence between CPolynomial and CMvPolynomial 1

This file establishes the ring equivalence CPolynomial.cmvEquiv : CPolynomial R ≃+* CMvPolynomial 1 R.

The equivalence chain is: CPolynomial R ≃ R[X] ≃ (CMvPolynomial 0 R)[X] ≃ CMvPolynomial 1 R

The bridge lemmas expose how the inverse equivalence interacts with evaluation and degree, so one-variable results proved for CPolynomial can be transported to callers that still use CMvPolynomial 1.

noncomputable def CompPoly.CPolynomial.cmvEquiv {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] : CPolynomial R ≃+* CPoly.CMvPolynomial 1 R

Ring equivalence between computable univariate polynomials and single-variable computable multivariate polynomials.

theorem CompPoly.CPolynomial.eval_cmvEquiv_symm {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] (p : CPoly.CMvPolynomial 1 R) (x : R) : eval x (cmvEquiv.symm p) = CPoly.CMvPolynomial.eval (fun (x_1 : Fin 1) => x) p

Evaluation after converting a single-variable CMvPolynomial back to CPolynomial agrees with multivariate evaluation at the constant assignment.

theorem CompPoly.CPolynomial.natDegree_cmvEquiv_symm_sub {R : Type u_1} [CommRing R] [BEq R] [LawfulBEq R] [Nontrivial R] (p q : CPoly.CMvPolynomial 1 R) : (cmvEquiv.symm p - cmvEquiv.symm q).natDegree = MvPolynomial.degreeOf 0 (CPoly.fromCMvPolynomial p - CPoly.fromCMvPolynomial q)

Degree transport for differences through the inverse of cmvEquiv.