Theorems · Theorem · commutative algebra

List.toFinsupp_append

∀ {R : Type u_2} [inst : AddZeroClass R] (l₁ l₂ : List R) [inst_1 : DecidablePred fun x => (l₁ ++ l₂).getD x 0 ≠ 0]
  [inst_2 : DecidablePred fun x => l₁.getD x 0 ≠ 0] [inst_3 : DecidablePred fun x => l₂.getD x 0 ≠ 0],
  (l₁ ++ l₂).toFinsupp = l₁.toFinsupp + Finsupp.embDomain (addLeftEmbedding l₁.length) l₂.toFinsupp

Defined in

Mathlib.Data.List.ToFinsupp

Cited by

2 results in Mathlib

Foundations

Depth 67 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddZeroClassDecidablePredDecidablePredDecidablePred