catalan_two

Mathlib.Combinatorics.Enumerative.Catalan

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

English

The second Catalan number equals 2.

Русский

Вторая цифра Каталана равна 2.

LaTeX

$$$ catalan(2) = 2 $$$

Lean4

theorem catalan_two : catalan 2 = 2 := by norm_num [catalan_eq_centralBinom_div, Nat.centralBinom, Nat.choose]

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

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

Разделы

Аффилиация

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