English
For any d, invOneSubPow S d equals the inverse of (1 − X)^d; hence its inverse is (1 − X)^d.
Русский
Для любого d invOneSubPow S d — обратная к (1 − X)^d; следовательно, её обратная равна (1 − X)^d.
LaTeX
$$$$ invOneSubPow\, S\, d = (1 - X)^{{-d}} \quad (\text{as a power series}) $$$$
Lean4
/-- The theorem `PowerSeries.mk_one_mul_one_sub_eq_one` implies that `1 - X` is a unit in `S⟦X⟧`
whose inverse is the power series `1 + X + X^2 + ...`. This theorem states that for any `d : ℕ`,
`PowerSeries.invOneSubPow S d` is equal to `(1 - X)⁻¹ ^ d`.
-/
theorem invOneSubPow_eq_inv_one_sub_pow :
invOneSubPow S d =
(Units.mkOfMulEqOne (1 - X) (mk 1 : S⟦X⟧) <| Eq.trans (mul_comm _ _) (mk_one_mul_one_sub_eq_one S))⁻¹ ^ d :=
by
induction d with
| zero => exact Eq.symm <| pow_zero _
| succ d _ =>
rw [inv_pow]
exact
(DivisionMonoid.inv_eq_of_mul _ (invOneSubPow S (d + 1)) <|
by
rw [← Units.val_eq_one, Units.val_mul, Units.val_pow_eq_pow_val]
exact (invOneSubPow S (d + 1)).inv_val).symm
