Documentation

CompPoly.Multivariate.MvPolyEquiv.Instances

CMvPolynomial/MvPolynomial Instances #

Compatibility lemmas used to transport algebraic structure across the conversion.

source
@[simp]
theorem CPoly.map_add {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (a b : CMvPolynomial n R) :
fromCMvPolynomial (a + b) = fromCMvPolynomial a + fromCMvPolynomial b
source
@[simp]
theorem CPoly.map_zero {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
fromCMvPolynomial 0 = 0
source
instance CPoly.instTransCmpNatCompareOfLessAndEq_compPoly :
Std.TransCmp fun (x y : ℕ) => compareOfLessAndEq x y
source
instance CPoly.instTransCmpCMvMonomialCompareLexNatCompareOfLessAndEq {n : ℕ} :
Std.TransCmp (Vector.compareLex fun (x y : ℕ) => compareOfLessAndEq x y)
source
@[simp]
theorem CPoly.map_one {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
fromCMvPolynomial 1 = 1
source
@[instance_reducible]
instance CPoly.instAddCommSemigroupCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
AddCommSemigroup (CMvPolynomial n R)
source
@[instance_reducible]
instance CPoly.instAddMonoidCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
AddMonoid (CMvPolynomial n R)
source
@[instance_reducible]
instance CPoly.instAddCommMonoidCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
AddCommMonoid (CMvPolynomial n R)
source
theorem CPoly.toList_pairs_monomial_coeff {n : ℕ} {R : Type u_1} [CommSemiring R] {β : Type u_2} [AddCommMonoid β] {t : Unlawful n R} {f : CMvMonomial n → R → β} :
List.map (fun (term : CMvMonomial n × R) => f term.1 term.2) (Std.ExtTreeMap.toList t) = List.map (fun (m : CMvMonomial n) => f m (Unlawful.coeff m t)) t.monomials
source
theorem CPoly.foldl_eq_sum {n : ℕ} {R : Type u_1} [CommSemiring R] {β : Type u_2} [AddCommMonoid β] {t : CMvPolynomial n R} {f : CMvMonomial n → R → β} :
Std.ExtTreeMap.foldl (fun (x : β) (m : CMvMonomial n) (c : R) => f m c + x) 0 ↑t = (fromCMvPolynomial t).coeff.sum (f ∘ CMvMonomial.ofFinsupp)
source
theorem CPoly.coeff_sum {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {α : Type u_2} [AddCommMonoid α] (s : Finset α) (f : α → CMvPolynomial n R) (m : CMvMonomial n) :
CMvPolynomial.coeff m (∑ x ∈ s, f x) = ∑ x ∈ s, CMvPolynomial.coeff m (f x)
source
theorem CPoly.fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {f : (Fin n →₀ ℕ) → R → Lawful n R} {a : CMvPolynomial n R} :
fromCMvPolynomial ((fromCMvPolynomial a).coeff.sum f) = (fromCMvPolynomial a).coeff.sum fun (m : Fin n →₀ ℕ) (c : R) => fromCMvPolynomial (f m c)
source
@[simp]
theorem CPoly.map_mul {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (a b : CMvPolynomial n R) :
fromCMvPolynomial (a * b) = fromCMvPolynomial a * fromCMvPolynomial b
source
@[instance_reducible]
instance CPoly.instMonoidWithZeroCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
MonoidWithZero (CMvPolynomial n R)
source
@[instance_reducible]
instance CPoly.instSemiringCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
Semiring (CMvPolynomial n R)
source
@[instance_reducible]
instance CPoly.instCommSemiringCMvPolynomial {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {n : ℕ} :
CommSemiring (CMvPolynomial n R)
source
@[simp]
theorem CPoly.map_neg {n : ℕ} {R : Type u_2} [CommRing R] [BEq R] [LawfulBEq R] (a : CMvPolynomial n R) :
fromCMvPolynomial (-a) = -fromCMvPolynomial a
source
theorem CPoly.map_sub {n : ℕ} {R : Type u_2} [CommRing R] [BEq R] [LawfulBEq R] (a b : CMvPolynomial n R) :
fromCMvPolynomial (Sub.sub a b) = fromCMvPolynomial a - fromCMvPolynomial b
source
@[instance_reducible]
instance CPoly.instCommRingCMvPolynomial {n : ℕ} {R : Type u_2} [CommRing R] [BEq R] [LawfulBEq R] :
CommRing (CMvPolynomial n R)
source
noncomputable def CPoly.polyRingEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
CMvPolynomial n R ≃+* MvPolynomial (Fin n) R
Instances For
    source
    theorem CPoly.coe_polyRingEquiv {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
    ⇑polyRingEquiv = fromCMvPolynomial

    The underlying function of polyRingEquiv is the computable fromCMvPolynomial.

    source
    noncomputable def CPoly.CMvPolynomial.isEmptyRingEquiv {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
    CMvPolynomial 0 R ≃+* R

    Ring equivalence between CMvPolynomial 0 R and R.

    Instances For
      source
      instance CPoly.CMvPolynomial.instNontrivial {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] [Nontrivial R] :
      Nontrivial (CMvPolynomial n R)
      source
      @[instance_reducible]
      instance CPoly.CMvPolynomial.instSMul {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
      SMul R (CMvPolynomial n R)
      source
      @[instance_reducible]
      instance CPoly.CMvPolynomial.instSMulZeroClass {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
      SMulZeroClass R (CMvPolynomial n R)
      source
      @[simp]
      theorem CPoly.CMvPolynomial.smul_def {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (r : R) (p : CMvPolynomial n R) :
      r • p = C r * p
      source
      theorem CPoly.CMvPolynomial.fromCMvPolynomial_C {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (r : R) :
      fromCMvPolynomial (C r) = MvPolynomial.C r
      source
      def CPoly.CMvPolynomial.CHom {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
      R →+* CMvPolynomial n R

      CMvPolynomial.C bundled as a ring homomorphism. Computable.

      Instances For
        source
        @[simp]
        theorem CPoly.CMvPolynomial.CHom_apply {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] (c : R) :
        CHom c = C c
        source
        theorem CPoly.CMvPolynomial.fromCMvPolynomial_sum {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {ι : Type u_2} (s : Finset ι) (f : ι → CMvPolynomial n R) :
        fromCMvPolynomial (∑ i ∈ s, f i) = ∑ i ∈ s, fromCMvPolynomial (f i)

        fromCMvPolynomial commutes with a finite sum.

        source
        theorem CPoly.CMvPolynomial.fromCMvPolynomial_prod {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] {ι : Type u_2} (s : Finset ι) (f : ι → CMvPolynomial n R) :
        fromCMvPolynomial (∏ i ∈ s, f i) = ∏ i ∈ s, fromCMvPolynomial (f i)

        fromCMvPolynomial commutes with a finite product.

        source
        @[instance_reducible]
        noncomputable instance CPoly.CMvPolynomial.instAlgebra {n : ℕ} {R : Type u_1} [CommSemiring R] [BEq R] [LawfulBEq R] :
        Algebra R (CMvPolynomial n R)