Theorems · Theorem · commutative algebra

List.toFinsupp_concat_eq_toFinsupp_add_single

∀ {R : Type u_2} [inst : AddZeroClass R] (x : R) (xs : List R)
  [inst_1 : DecidablePred fun i => (xs ++ [x]).getD i 0 ≠ 0] [inst_2 : DecidablePred fun i => xs.getD i 0 ≠ 0],
  (xs ++ [x]).toFinsupp = xs.toFinsupp + fun₀ | xs.length => x

Defined in

Mathlib.Data.List.ToFinsupp

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddZeroClassDecidablePredDecidablePred