# mathlibdocumentation

field_theory.tower

# 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: module.rank which gives the dimension of an arbitrary vector space as a cardinal, and finite_dimensional.finrank which gives the dimension of a finitely-dimensional vector space as a natural number.

## Tags #

tower law

theorem dim_mul_dim' (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [ K] [ A] [ A] [ A] :
K).lift * A).lift = A).lift

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).

theorem dim_mul_dim (F : Type u) (K A : Type v) [field F] [field K] [ K] [ A] [ A] [ A] :
K * A = 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).

theorem finite_dimensional.trans (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [ K] [ A] [ A] [ A] [ K] [ A] :
theorem finite_dimensional.right (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [ K] [ A] [ A] [ A] [hf : A] :
theorem finite_dimensional.finrank_mul_finrank (F : Type u) (K : Type v) (A : Type w) [field F] [field K] [ K] [ A] [ A] [ A] [ K] :

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).

@[protected, instance]
def finite_dimensional.linear_map (F : Type u) (V : Type v) (W : Type w) [field F] [ V] [ W] [ V] [ W] :
(V →ₗ[F] W)
theorem finite_dimensional.finrank_linear_map (F : Type u) (V : Type v) (W : Type w) [field F] [ V] [ W] [ V] [ W] :
@[protected, instance]
def finite_dimensional.linear_map' (F : Type u) (K : Type v) (V : Type w) [field F] [field K] [ K] [ K] [ V] [ V] :
(V →ₗ[F] K)
theorem finite_dimensional.finrank_linear_map' (F : Type u) (K : Type v) (V : Type w) [field F] [field K] [ K] [ K] [ V] [ V] :