CMvPolynomial/MvPolynomial Core

Core conversions between CMvPolynomial and MvPolynomial.

def CPoly.fromCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] (p : CMvPolynomial n R) : MvPolynomial (Fin n) R

noncomputable def CPoly.toCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] (p : MvPolynomial (Fin n) R) : CMvPolynomial n R

@[instance_reducible]

instance CPoly.instMembershipVectorNatUnlawful {n : ℕ} {R : Type u_2} : Membership (Vector ℕ n) (Unlawful n R)

@[simp]

theorem CPoly.toCMvPolynomial_fromCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] {p : CMvPolynomial n R} : toCMvPolynomial (fromCMvPolynomial p) = p

@[simp]

theorem CPoly.fromCMvPolynomial_toCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] {p : MvPolynomial (Fin n) R} : fromCMvPolynomial (toCMvPolynomial p) = p

theorem CPoly.fromCMvPolynomial_injective {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] : Function.Injective fromCMvPolynomial

theorem CPoly.coeff_eq {n : ℕ} {R : Type u_1} [CommSemiring R] {m : Fin n →₀ ℕ} (a : CMvPolynomial n R) : (fromCMvPolynomial a).coeff m = CMvPolynomial.coeff (CMvMonomial.ofFinsupp m) a

theorem CPoly.eq_iff_fromCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {u v : CMvPolynomial n R} : u = v ↔ fromCMvPolynomial u = fromCMvPolynomial v

noncomputable def CPoly.polyEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] : CMvPolynomial n R ≃ MvPolynomial (Fin n) R