coeff_pow_p'

Mathlib.RingTheory.Perfection

URI: https://scilib.ai/kg/mathlib#Perfection.coeff_pow_p'

English

Let f be as above and n ∈ ℕ. Then coeff R p (n+1) f^p = coeff R p n f.

Русский

Пусть f удовлетворяет условиям; тогда коэффициент при (n+1) для (f)^p равен коэффициентy при n для f.

LaTeX

$$$\\operatorname{coeff} R p (n+1) f^p = \\operatorname{coeff} R p n f$$$

Lean4

theorem coeff_pow_p' (f : Ring.Perfection R p) (n : ℕ) : coeff R p (n + 1) f ^ p = coeff R p n f :=
  f.2 n

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

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

Разделы

Аффилиация

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