Theorems · Theorem · combinatorics

Finset.nsmul_piAntidiag

∀ {ι : Type u_1} [inst : DecidableEq ι] [inst_1 : DecidableEq (ι → ℕ)] (s : Finset ι) (m : ℕ) {n : ℕ},
  n ≠ 0 → n • s.piAntidiag m = {f ∈ s.piAntidiag (n * m) | ∀ i ∈ s, n ∣ f i}

Defined in

Mathlib.Algebra.Order.Antidiag.Pi

Cited by

2 results in Mathlib

Foundations

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

Assumes

DecidableEqDecidableEq