Theorems · Theorem · combinatorics

Finset.map_nsmul_piAntidiag_univ

∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : Fintype ι] (m : ℕ) {n : ℕ} (hn : n ≠ 0),
  Finset.map { toFun := fun x => n • x, inj' := ⋯ } (Finset.univ.piAntidiag m) =
    {f ∈ Finset.univ.piAntidiag (n * m) | ∀ (i : ι), n ∣ f i}

Defined in

Mathlib.Algebra.Order.Antidiag.Pi

Cited by

0 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype