homogeneousComponent_of_order

Mathlib.RingTheory.MvPowerSeries.Order

URI: https://scilib.ai/kg/mathlib#MvPowerSeries.homogeneousComponent_of_order

← MathLib Explorer

English

If p equals the order of f, then the p-th homogeneous component is nonzero.

Русский

Если p равно порядку f, то p-я однородная компонента ненулевая.

LaTeX

$$p = f.order → homogeneousComponent(p) f ≠ 0$$

Lean4

theorem homogeneousComponent_of_order {f : MvPowerSeries σ R} {p : ℕ} (hf : p = f.order) :
    f.homogeneousComponent p ≠ 0 :=
  weightedHomogeneousComponent_of_weightedOrder hf

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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