catalan_three

Mathlib.Combinatorics.Enumerative.Catalan

URI: https://scilib.ai/kg/mathlib#catalan_three

English

Let C_n denote the Catalan numbers. Then C_3 = 5.

Русский

Пусть C_n обозначает числа Каталана. Тогда C_3 = 5.

LaTeX

$$$C_3 = 5$$$

Lean4

theorem catalan_three : catalan 3 = 5 := by norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

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

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

Разделы

Аффилиация

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