map_zero

Mathlib.Combinatorics.Additive.AP.Three.Behrend

URI: https://scilib.ai/kg/mathlib#Behrend.map_zero

English

For any d, map(d) is zero on the unique function a: Fin 0 → ℕ (the empty input).

Русский

Для любого d отображение map(d) равно нулю на единичной функции a: Fin 0 → ℕ (пустой вход).

LaTeX

$$$ map(d) \\big|_{Fin 0 \\to \\mathbb{N}} = 0 $$$

Lean4

theorem map_zero (d : ℕ) (a : Fin 0 → ℕ) : map d a = 0 := by simp [map]

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

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

Разделы

Аффилиация

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