First of all, I apologize if this is too elementary for MO. I am reposting this from MSE where I asked this question two days ago (link to MSE post).
I've been wondering about the following thing. Let $A$ be a commutative ring (with unit) such that $A[[T]]$ is Noetherian. Can we conclude that $A[T]$ is Noetherian without invoking Hilbert's Basis Theorem (or a similar argument)? In other words, if we know Noetherianity of the power series ring, do we get Noetherianity of the polynomial ring "for almost free"?
Notice that the canonical epimorphism $A[[T]]\twoheadrightarrow A$ gives us the Noetherian property for $A$, which then implies Noetherianity of $A[T]$ by the usual polynomial Hilbert Basis Theorem (HBT for short). However, if we wish to skip HBT, the implication is non-obvious (at least to me) since Noetherianity is not "inclusion-borne". Moreover, notice that the opposite direction does not require HBT as $A[[T]]$ is the $(T)$-adic completion of $A[T]$.
All the standard texts on Commutative Algebra (AM, Kaplansky, Matsumura, Zariski-Samuel) appear to give separate proofs one way or another. Even though the proofs of both cases are deceivingly similar and polynomials are a special case of power series, both theorems seem content-wise quite distant from each other.