Let $\mathbb{F}$ be a field and let $(a_n)_{n \geq 0}$, $(b_n)_{n \geq 0}$ be two linear recurrences with terms in $\mathbb{F}$ and respective characteristic polynomials $f(X), g(X) \in \mathbb{F}[X]$. Put $c_n := a_n b_n$ for all integers $n \geq 0$. It is well-known than $(c_n)_{n \geq 0}$ is a linear recurrence.
Answering ME question 1348838, Julian Rosen claimed (and proved) that a characteristic polynomial for $(c_n)_{n \geq 0}$ is given by $h(x) := \operatorname{Res}_Y(f(Y), Y^{\deg(g)}g(X/Y))$, where $\operatorname{Res}_Y$ is the resultant respect to $Y$. In truth, the proof was given for $\mathbb{F} = \mathbb{C}$, but no step refers to particular properties of the complex numbers, so the claim holds in any field.
Looking on the classic book on linear recurrences [1], I could not find Rosen's result. Neither I found it in [2] (for linear recurrences on finite fields).
Does someone have a reference for it?
Thank you very much.
[1] G. Everest, A. van der Poorten, I. E. Shparlinski, and T. Ward - Recurrence Sequences
[2] R. Lidl and H. Niederreiter - Introduction to Finite Fields and Their Applications
