invOneSubPow_add

Mathlib.RingTheory.PowerSeries.WellKnown

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

← MathLib Explorer

English

For all d,e, invOneSubPow S (d+e) = invOneSubPow S d · invOneSubPow S e.

Русский

Для любых d, e: invOneSubPow S (d+e) = invOneSubPow S d · invOneSubPow S e.

LaTeX

$$$$ invOneSubPow\, S\ (d+e) = invOneSubPow\, S\, d \cdot invOneSubPow\, S\, e $$$$

Lean4

theorem invOneSubPow_add (e : ℕ) : invOneSubPow S (d + e) = invOneSubPow S d * invOneSubPow S e := by
  simp_rw [invOneSubPow_eq_inv_one_sub_pow, pow_add]

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

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

Разделы

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

Аффилиация

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