coeff_div

Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

URI: https://scilib.ai/kg/mathlib#PowerSeries.IsWeierstrassDivisorAt.coeff_div

English

For [IsPrecomplete I A], the i-th coefficient of the divisor f satisfies coeff_i(H.div f) = (H.divCoeff f i).1.

Русский

Для [IsPrecomplete I A] выполняется то же соотношение: coeff_i(H.div f) = (H.divCoeff f i).1.

LaTeX

$$$ \\operatorname{coeff}_i\\bigl(H.\\div f\\bigr) = (H.\\divCoeff f i).1. $$$

Lean4

theorem coeff_div [IsPrecomplete I A] (i : ℕ) : coeff i (H.div f) = (H.divCoeff f i).1 := by simp [div]

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

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

Разделы

Аффилиация

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