Un'estensione finita è finitamente generata?

[Giorgeous]

Buonasera. Come da oggetto, data un'estensione di campi L/K, è vero che se tale estensione è finita, allora è finitamente generata? Perché a me hanno fornito questa dimostrazione, che mi sembra corretta. La ragione per cui lo chiedo è solo che nessuno mi ha citato questa cosa nei vari corsi di algebra, nonostante mi sembri una cosa importante. Ecco la dimostrazione:

Prendiamo un elemento a1 in L-K, e consideriamo K(a1). L'elemento a1 non è in K, perciò K(a1) ha su K dimensione almeno 2. Prendiamo un elemento a2 in L-K(a1),poi un elemento a3 in L-K(a1,a2) e così via. Per la formula del grado, abbiamo che [L:K] =[L:K(a1,a2,...,an)][K(a1,a2,...,an):K(a1,a2,...,an-1)]...[K(a1,a2,a3):K(a1,a2)] [K(a1,a2):K(a1)] [K(a1):K]
Poiché il grado di L/K è finito, necessariamente abbiamo un numero finito di generatori, cvd

[Martino]

Se con "finitamente generata" intendi come spazio vettoriale allora è ovvio, è la definizione stessa di estensione finita (un'estensione L/K si dice finita se L ha dimensione finita su K, cioè se esiste una K-base finita di L).

[Giorgeous]

In realtà intendevo come campo generato da un numero finito di elementi

[Martino]

Ah sì ma è chiaro che se L è finitamente generato su K come spazio vettoriale allora è anche finitamente generato su K come campo. Infatti qualsiasi campo che contiene K e un insieme X di elementi contiene anche tutte le combinazioni lineari degli elementi di X su K.