Theorems · Definition · combinatorics

Finset.finAntidiagonal.aux

{μ : Type u_2} →
  [inst : AddCommMonoid μ] →
    [Finset.HasAntidiagonal μ] → [DecidableEq μ] → (d : ℕ) → (n : μ) → { s // ∀ (f : Fin d → μ), f ∈ s ↔ ∑ i, f i = n }

Auxiliary construction for finAntidiagonal that bundles a proof of lawfulness (mem_finAntidiagonal), as this is needed to invoke disjiUnion. Using Finset.disjiUnion makes this computationally much more efficient than using Finset.biUnion.

Defined in

Mathlib.Algebra.Order.Antidiag.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddCommMonoidFinset.HasAntidiagonalDecidableEq