Theorems · Definition · combinatorics

Finset.finsuppAntidiagEquivSubtype

{ι : Type u_1} →
  {μ : Type u_2} →
    [inst : DecidableEq ι] →
      [inst_1 : AddCommMonoid μ] →
        [inst_2 : Finset.HasAntidiagonal μ] →
          [inst_3 : DecidableEq μ] →
            (s : Finset ι) → (n : μ) → ↥(s.finsuppAntidiag n) ≃ { P // (P.sum fun x => id) = n }

The equivalence between Finset.finsuppAntidiag s n and the subtype of s →₀ μ whose sum is n.

Defined in

Mathlib.Algebra.Order.Antidiag.FinsuppEquiv

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqAddCommMonoidFinset.HasAntidiagonalDecidableEq