antidiagonalTuple — Mathlib

English

The multiset antidiagonalTuple k n is defined as the multiset corresponding to List.Nat.antidiagonalTuple k n.

Русский

Мультимножество antidiagonalTuple k n задаётся как мультимножество, соответствующее списку List.Nat.antidiagonalTuple k n.

LaTeX

$$$ antidiagonalTuple (k n) = List.Nat.antidiagonalTuple k n $$$

Lean4

/-- `Multiset.Nat.antidiagonalTuple k n` is a multiset of `k`-tuples summing to `n` -/
def antidiagonalTuple (k n : ℕ) : Multiset (Fin k → ℕ) :=
  List.Nat.antidiagonalTuple k n

Похожие утверждения