Theorems · Theorem · combinatorics

Finsupp.antidiagonal_single

∀ {α : Type u} [inst : DecidableEq α] (a : α) (n : ℕ),
  (Finset.HasAntidiagonal.antidiagonal fun₀ | a => n) =
    Finset.map ({ toFun := Finsupp.single a, inj' := ⋯ }.prodMap { toFun := Finsupp.single a, inj' := ⋯ })
      (Finset.HasAntidiagonal.antidiagonal n)

Defined in

Mathlib.Data.Finsupp.Antidiagonal

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEq