antidiagonalTuple_zero_zero — Mathlib

English

In the Finset version, the 0-0 antidiagonal is the singleton containing the all-zero 0-tuple.

Русский

В версии Finset антидиагональ 0-0 представляет собой единичный элемент, содержащий нулевой 0‑кортеж.

LaTeX

$$$ \operatorname{antidiagonalTuple}_{\mathrm{Finset}}(0,0) = \{ \mathbf{0}_{0} \}. $$$

Lean4

@[simp]
theorem antidiagonalTuple_zero_zero : antidiagonalTuple 0 0 = {![]} :=
  rfl

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