Intermediate field extension

Suppose $𝐹 : 𝐿 : 𝐾$ is a tower of field extensions

𝐹 | 𝐿 | 𝐾

Then in particular one has a Vector space over a field extension, whence

[𝐹 : 𝐾] = [𝐹 : 𝐿] [𝐿 : 𝐾]

and $𝐹 : 𝐾$ is finite iff both $𝐹 : 𝐿$ and $𝐿 : 𝐾$ are. #m/thm/field

Corollaries of this corollary

Given a tower $𝐹 : 𝐿 : 𝐾$ , it follows both $[𝐹 : 𝐾]$ and $[𝐹 : 𝐿]$ divide $[𝐹 : 𝐾]$ .

#state/tidy | #lang/en | #SemBr