Lax Lean Archive

Proof of `Formal power series` (3rd statement)

groundedproofs/Lax619925Proofs/Series.lean · lax-619925

What this proof establishes

no assumptions

def✓Lax619925.Series (3rd statement)

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Reversal interchanges the left and right derivatives: the coefficient of a⋅wa · w in ff, read off reversalfreversal f, is the coefficient of w⋅aw · a, and (w++[a]).reverse=a::w.reverse(w ++ [a]).reverse = a :: w.reverse.