antidiagonal — Mathlib

English

The antidiagonal of a natural number n is the multiset of pairs (i, j) of natural numbers such that i + j = n.

Русский

Антидиагональ натурального числа n — это мультимножество пар (i, j) таких, что i + j = n.

LaTeX

$$$\\mathrm{antidiagonal}(n) = \\{(i,j) \\in \\mathbb{N}\\times\\mathbb{N} \\mid i+j=n\\}$ (мультимножество).$$$

Lean4

/-- The antidiagonal of a natural number `n` is
    the multiset of pairs `(i, j)` such that `i + j = n`. -/
def antidiagonal (n : ℕ) : Multiset (ℕ × ℕ) :=
  List.Nat.antidiagonal n

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