def Hex.MvPoly.Kernel.CoeffMap.map {α : Type u} {β : Type v} (f : α → β) (p : PolyList α) : PolyList β

Change the coefficient representation without changing support.

Equations

• Hex.MvPoly.Kernel.CoeffMap.map f p = List.map (fun (t : Hex.MvPoly.Kernel.Term α) => (t.fst, f t.snd)) p

@[simp]

theorem Hex.MvPoly.Kernel.CoeffMap.map_nil {α : Type u} {β : Type v} (f : α → β) : map f [] = []

@[simp]

theorem Hex.MvPoly.Kernel.CoeffMap.map_cons {α : Type u} {β : Type v} (f : α → β) (t : Term α) (ts : PolyList α) : map f (t :: ts) = (t.fst, f t.snd) :: map f ts

@[simp]

theorem Hex.MvPoly.Kernel.CoeffMap.map_map {α : Type u} {β : Type v} {γ : Type w} (g : β → γ) (f : α → β) (p : PolyList α) : map g (map f p) = map (fun (a : α) => g (f a)) p

theorem Hex.MvPoly.Kernel.CoeffMap.map_injective {α : Type u} {β : Type v} (f : α → β) (hf : Function.Injective f) : Function.Injective (map f)

theorem Hex.MvPoly.Kernel.CoeffMap.canonical_map {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) {n : Nat} {p : PolyList α} : Canonical n (map f p) ↔ Canonical n p

theorem Hex.MvPoly.Kernel.CoeffMap.map_insert {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (t : Term α) (p : PolyList α) : map f (insert t p) = insert (t.fst, f t.snd) (map f p)

theorem Hex.MvPoly.Kernel.CoeffMap.map_insertSum {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (p q : PolyList α) : map f (insertSum p q) = insertSum (map f p) (map f q)

theorem Hex.MvPoly.Kernel.CoeffMap.map_merge {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (fuel : Nat) (p q : PolyList α) : map f (merge fuel p q) = merge fuel (map f p) (map f q)

theorem Hex.MvPoly.Kernel.CoeffMap.map_add {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (p q : PolyList α) : map f (add p q) = add (map f p) (map f q)

theorem Hex.MvPoly.Kernel.CoeffMap.map_mapCoeffs {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] (g : α → α) (h : β → β) (hg : ∀ (a : α), f (g a) = h (f a)) (p : PolyList α) : map f (mapCoeffs g p) = mapCoeffs h (map f p)

theorem Hex.MvPoly.Kernel.CoeffMap.map_mulTerm {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) [Mul α] [Mul β] (hm : ∀ (a b : α), f (a * b) = f a * f b) (t : Term α) (p : PolyList α) : map f (mulTerm t p) = mulTerm (t.fst, f t.snd) (map f p)

theorem Hex.MvPoly.Kernel.CoeffMap.map_sumRows {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (ps : List (PolyList α)) : map f (sumRows ps) = sumRows (List.map (map f) ps)

theorem Hex.MvPoly.Kernel.CoeffMap.map_mergeRound {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (ps : List (PolyList α)) : List.map (map f) (mergeRound ps) = mergeRound (List.map (map f) ps)

theorem Hex.MvPoly.Kernel.CoeffMap.map_mergeRows {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) (fuel : Nat) (ps : List (PolyList α)) : map f (mergeRows fuel ps) = mergeRows fuel (List.map (map f) ps)

theorem Hex.MvPoly.Kernel.CoeffMap.map_mul {α : Type u} {β : Type v} [Zero α] [Zero β] (f : α → β) (hz : ∀ (a : α), f a = 0 ↔ a = 0) [DecidableEq α] [DecidableEq β] [Add α] [Add β] (ha : ∀ (a b : α), f (a + b) = f a + f b) [Mul α] [Mul β] (hm : ∀ (a b : α), f (a * b) = f a * f b) (p q : PolyList α) : map f (mul p q) = mul (map f p) (map f q)

theorem Hex.MvPoly.Kernel.coeffs_mapCoeffs {κ : Type u} [Zero κ] [DecidableEq κ] (P : κ → Prop) (f : κ → κ) (hf : ∀ (c : κ), P (f c)) (a : PolyList κ) (t : Term κ) : t ∈ mapCoeffs f a → P t.snd

Mapping coefficients preserves any predicate satisfied by the map's image.

theorem Hex.MvPoly.Kernel.coeffs_insert {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (t : Term κ) (a : PolyList κ) (ht : P t.snd) (ha : ∀ (u : Term κ), u ∈ a → P u.snd) (u : Term κ) : u ∈ insert t a → P u.snd

Insertion preserves a coefficient predicate closed under addition.

theorem Hex.MvPoly.Kernel.coeffs_insertSum {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (a b : PolyList κ) (ha : ∀ (t : Term κ), t ∈ a → P t.snd) (hb : ∀ (t : Term κ), t ∈ b → P t.snd) (t : Term κ) : t ∈ insertSum a b → P t.snd

Insertion summation preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_merge {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (fuel : Nat) (a b : PolyList κ) (ha : ∀ (t : Term κ), t ∈ a → P t.snd) (hb : ∀ (t : Term κ), t ∈ b → P t.snd) (t : Term κ) : t ∈ merge fuel a b → P t.snd

Every budgeted merge preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_add {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (a b : PolyList κ) (ha : ∀ (t : Term κ), t ∈ a → P t.snd) (hb : ∀ (t : Term κ), t ∈ b → P t.snd) (t : Term κ) : t ∈ add a b → P t.snd

Polynomial addition preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_sumRows {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (as : List (PolyList κ)) (ha : ∀ (a : PolyList κ), a ∈ as → ∀ (t : Term κ), t ∈ a → P t.snd) (t : Term κ) : t ∈ sumRows as → P t.snd

Summing rows preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_mergeRound {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (as : List (PolyList κ)) (ha : ∀ (a : PolyList κ), a ∈ as → ∀ (t : Term κ), t ∈ a → P t.snd) (a : PolyList κ) : a ∈ mergeRound as → ∀ (t : Term κ), t ∈ a → P t.snd

One round of pairwise row merging preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_mergeRows {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) (fuel : Nat) (as : List (PolyList κ)) (ha : ∀ (a : PolyList κ), a ∈ as → ∀ (t : Term κ), t ∈ a → P t.snd) (t : Term κ) : t ∈ mergeRows fuel as → P t.snd

Balanced row merging preserves a coefficient predicate.

theorem Hex.MvPoly.Kernel.coeffs_mulTerm {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) [Mul κ] (hmul : ∀ (a b : κ), P (a * b)) (t : Term κ) (a : PolyList κ) (u : Term κ) : u ∈ mulTerm t a → P u.snd

Translating a multiplication row preserves a predicate on products and sums.

theorem Hex.MvPoly.Kernel.coeffs_mul {κ : Type u} [Zero κ] [DecidableEq κ] [Add κ] (P : κ → Prop) (hadd : ∀ (a b : κ), P a → P b → P (a + b)) [Mul κ] (hmul : ∀ (a b : κ), P (a * b)) (a b : PolyList κ) (t : Term κ) : t ∈ mul a b → P t.snd

Multiplication preserves a predicate on products and sums.