coeff_pthRoot

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#Perfection.coeff_pthRoot

English

The nth coefficient of pthRoot(f) equals the (n+1)th coefficient of f.

Русский

n-й коэффициент pthRoot(f) равен (n+1)-й коэффициенту f.

LaTeX

$$coeff(R,p,n)(pthRoot(R,p) f) = coeff(R,p,n+1)(f)$$

Lean4

theorem coeff_pthRoot (f : Ring.Perfection R p) (n : ℕ) : coeff R p n (pthRoot R p f) = coeff R p (n + 1) f :=
  rfl

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

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

Разделы

Аффилиация

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