Theorems · Theorem · combinatorics

Finset.map_nsmul_piAntidiag

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

Defined in

Mathlib.Algebra.Order.Antidiag.Pi

Cited by

1 results in Mathlib

Foundations

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

Assumes

DecidableEq