antidiagonalTuple_zero_right

Mathlib.Data.Fin.Tuple.NatAntidiagonal

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

English

antidiagonalTuple(k,0) equals the singleton containing the all-zero k-tuple.

Русский

antidiagonalTuple(k,0) тождественно равен одиночному кортежу нулей размерности k.

LaTeX

$$$ \operatorname{antidiagonalTuple}(k,0) = \{ \mathbf{0}_k \}. $$$

Lean4

theorem antidiagonalTuple_zero_right (k : ℕ) : antidiagonalTuple k 0 = {0} :=
  congr_arg _ (List.Nat.antidiagonalTuple_zero_right k)

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

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

Разделы

Аффилиация

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