English
Let S be a commutative ring and X a formal indeterminate. In the formal power series ring S[[X]], the series 1 + X + X^2 + X^3 + … is the multiplicative inverse of 1 − X; equivalently, (1 + X + X^2 + …)(1 − X) = 1.
Русский
Пусть S — коммутативное кольцо и X — формальный индетминат. В кольце формальных степенных рядов S[[X]] ряд 1 + X + X^2 + X^3 + … является обратным к 1 − X; то есть (1 + X + X^2 + …)(1 − X) = 1.
LaTeX
$$$$ (1 + X + X^2 + \cdots)(1 - X) = 1 \quad \text{in } S[[X]] $$$$
Lean4
/-- (1 + X + X^2 + ...) * (1 - X) = 1.
Note that the power series `1 + X + X^2 + ...` is written as `mk 1` where `1` is the constant
function so that `mk 1` is the power series with all coefficients equal to one.
-/
theorem mk_one_mul_one_sub_eq_one : (mk 1 : S⟦X⟧) * (1 - X) = 1 :=
by
rw [mul_comm, PowerSeries.ext_iff]
intro n
cases n with
| zero => simp
| succ n => simp [sub_mul]
