antidiagonalTuple_one

Mathlib.Data.Fin.Tuple.NatAntidiagonal

URI: https://scilib.ai/kg/mathlib#Multiset.Nat.antidiagonalTuple_one

English

There is exactly one k-tuple of natural numbers summing to n when k = 1; it is the 1-tuple [n].

Русский

Для k = 1 единственный k‑кортеж суммой n есть 1‑кортеж [n].

LaTeX

$$$ \operatorname{antidiagonalTuple}(1,n) = \{ \langle n \rangle \}. $$$

Lean4

@[simp]
theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = {![n]} :=
  congr_arg _ (List.Nat.antidiagonalTuple_one n)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru