Let $E/F$ be a field extension. Reading a proof that $$ \alpha \text{ is algebraic over } F \implies [F[\alpha]:F] < \infty, $$ one might begin by considering an element $f(\alpha) \in F[\alpha]$ and its corresponding polynomial in $F[x]$. Then, if $n := \deg m$ where $m(x)$ is the minimal polynomial of $\alpha$ over $K$, Euclidean division shows that $\{ 1, \alpha, \ldots, \alpha^{n-1} \}$ is a generating set for the vector space $F[\alpha]$ over $F$.
Question: I believe that I can prove that $$ F[\alpha] = \left\{ \sum_{i=0}^n a_i \alpha^i : a_i \in F \right\}, $$ but since it seems to not have been proved or even mentioned before in the text, I wonder if it is supposed to be trivial?
I do know that there is a corresponding result for ideals. If $A$ is a ring and $E \subseteq A$ is a non-empty subset, we may define $(E)$ to be the smallest ideal of $A$ containing $E$, that is, $$ (E) := \bigcap_{\substack{J \text{ ideal} \\ J \supseteq E}} J. $$ Then one can prove (and does it) $$ (E) = \left\{ \sum_{k=1}^n r_k a_k : r_k \in A, a_k \in E \right\}. $$