Tower of field extensions
In this file we prove the tower law for arbitrary extensions and finite extensions.
Suppose L is a field extension of K and K is a field extension of F.
Then [L:F] = [L:K] [K:F] where [E₁:E₂] means the E₂-dimension of E₁.
In fact we generalize it to vector spaces, where L is not necessarily a field,
but just a vector space over K.
Implementation notes
We prove two versions, since there are two notions of dimensions: vector_space.dim which gives
the dimension of an arbitrary vector space as a cardinal, and finite_dimensional.findim which
gives the dimension of a finitely-dimensional vector space as a natural number.
Tags
tower law
Tower law: if A is a K-vector space and K is a field extension of F then
dim_F(A) = dim_F(K) * dim_K(A).
Tower law: if A is a K-vector space and K is a field extension of F then
dim_F(A) = dim_F(K) * dim_K(A).
Tower law: if A is a K-algebra and K is a field extension of F then
dim_F(A) = dim_F(K) * dim_K(A).