nodup_antidiagonal

Mathlib.Data.List.NatAntidiagonal

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

← MathLib Explorer

English

The antidiagonal of n contains no duplicates.

Русский

Антидиагональ числа n не содержит повторяющихся элементов.

LaTeX

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

Lean4

/-- The antidiagonal of `n` does not contain duplicate entries. -/
theorem nodup_antidiagonal (n : ℕ) : Nodup (antidiagonal n) :=
  nodup_range.map ((@LeftInverse.injective ℕ (ℕ × ℕ) Prod.fst fun i ↦ (i, n - i)) fun _ ↦ rfl)

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

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

Разделы

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

Аффилиация

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