one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow

Mathlib.RingTheory.PowerSeries.WellKnown

URI: https://scilib.ai/kg/mathlib#PowerSeries.one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow

← MathLib Explorer

English

For all e, (1 - X)^{d+e} · (invOneSubPow S e).val = (1 - X)^d.

Русский

Для любого e: (1 - X)^{d+e} · (invOneSubPow S e).val = (1 - X)^d.

LaTeX

$$$$ (1 - X)^{d+e} \cdot (invOneSubPow\, S\, e).\text{val} = (1 - X)^d $$$$

Lean4

theorem one_sub_pow_add_mul_invOneSubPow_val_eq_one_sub_pow (e : ℕ) :
    (1 - X) ^ (d + e) * (invOneSubPow S e).val = (1 - X) ^ d := by
  simp [pow_add, mul_assoc, ← invOneSubPow_inv_eq_one_sub_pow S e]

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

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

Разделы

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

Аффилиация

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