Mathlib

A formal power series is an infinite list of coefficients, no convergence asked.