invOneSubPow_val_one_eq_invUnitSub_one

English

The series (1 − X)^{-1} equals the geometric series 1 + X + X^2 + …; equivalently, its coefficients are all 1.

Русский

Обратная к 1 − X равна геометрическому ряду 1 + X + X^2 + …; коэффициенты при X^n равны 1.

LaTeX

$$$$ (1 - X)^{-1} = 1 + X + X^2 + \cdots, $$$$

Lean4

theorem invOneSubPow_val_one_eq_invUnitSub_one : (invOneSubPow S 1).val = invUnitsSub (1 : Sˣ) := by
  simp [invOneSubPow, invUnitsSub]

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