nodup_antidiagonal

Mathlib.Data.Multiset.NatAntidiagonal

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

← MathLib Explorer

English

The antidiagonal of any natural number has no duplicates as a multiset.

Русский

У антидиагонали любого n нет повторяющихся элементов.

LaTeX

$$$\\operatorname{Nodup}(\\mathrm{antidiagonal}(n)).$$$

Lean4

/-- The antidiagonal of `n` does not contain duplicate entries. -/
@[simp]
theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
  coe_nodup.2 <| List.Nat.nodup_antidiagonal n

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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