z_last

Mathlib.Analysis.SpecialFunctions.Bernstein

URI: https://scilib.ai/kg/mathlib#bernstein.z_last

English

For every positive integer n, the last Bernstein coefficient divided by n equals 1.

Русский

Для каждого положительного целого n последняя коэффициента Бернштейна, делённая на n, равна единице.

LaTeX

$$$\\frac{\\text{last}_n}{n} = 1 \\quad (n>0).$$$

Lean4

@[simp]
theorem z_last {n : ℕ} (hn : n ≠ 0) : .last n/ₙ = 1 := by simp [z, hn]

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

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

Разделы

Аффилиация

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