Finite linear independence of formal power series survives arbitrary field extension. A finite nonzero coefficient minor witnesses independence.

theorem CCDN.powerSeries_linearIndependent_map_of_linearIndependent {K : Type u_1} {L : Type u_2} {ι : Type u_3} [Field K] [Field L] [Algebra K L] (v : ι → PowerSeries K) (hv : LinearIndependent K v) : LinearIndependent L fun (i : ι) => (PowerSeries.map (algebraMap K L)) (v i)

Independence survives coefficient extension even for an infinite family: each relation involves only a finite subfamily.