finMulAntidiag_zero_left

Mathlib.Algebra.Order.Antidiag.Nat

URI: https://scilib.ai/kg/mathlib#Nat.finMulAntidiag_zero_left

English

If n ≠ 1, then finMulAntidiag 0 n is empty.

Русский

Если n ≠ 1, то finMulAntidiag 0 n пусто.

LaTeX

$$$\text{finMulAntidiag}(0,n)=\emptyset\quad\text{если } n\neq 1$$$

Lean4

theorem finMulAntidiag_zero_left {n : ℕ} (hn : n ≠ 1) : finMulAntidiag 0 n = ∅ :=
  by
  ext
  simp [hn.symm]

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

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

Разделы

Аффилиация

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