chore(field_theory/adjoin): move dim/findim lemmas (#5342)

adjoin.lean has some dim/findim lemmas, some of which could be moved to intermediate_field.lean

Author: tb65536

src/field_theory/adjoin.lean

@@ -342,26 +342,24 @@ adjoin_simple_eq_bot_iff.mpr (coe_int_mem ⊥ n)
 section adjoin_dim
 open finite_dimensional vector_space
 
-@[simp] lemma dim_intermediate_field_eq_dim_subalgebra :
-  dim F (adjoin F S).to_subalgebra = dim F (adjoin F S) := rfl
+variables {K L : intermediate_field F E}
 
-@[simp] lemma findim_intermediate_field_eq_findim_subalgebra :
-  findim F (adjoin F S).to_subalgebra = findim F (adjoin F S) := rfl
+@[simp] lemma dim_eq_one_iff : dim F K = 1 ↔ K = ⊥ :=
+by rw [← to_subalgebra_eq_iff, ← dim_eq_dim_subalgebra,
+  subalgebra.dim_eq_one_iff, bot_to_subalgebra]
 
-@[simp] lemma to_subalgebra_eq_iff {K L : intermediate_field F E} :
-  K.to_subalgebra = L.to_subalgebra ↔ K = L :=
-by { rw [subalgebra.ext_iff, intermediate_field.ext'_iff, set.ext_iff], refl }
+@[simp] lemma findim_eq_one_iff : findim F K = 1 ↔ K = ⊥ :=
+by rw [← to_subalgebra_eq_iff, ← findim_eq_findim_subalgebra,
+  subalgebra.findim_eq_one_iff, bot_to_subalgebra]
 
 lemma dim_adjoin_eq_one_iff : dim F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
-by rw [←dim_intermediate_field_eq_dim_subalgebra, subalgebra.dim_eq_one_iff,
-      ←bot_to_subalgebra, to_subalgebra_eq_iff, adjoin_eq_bot_iff]
+iff.trans dim_eq_one_iff adjoin_eq_bot_iff
 
 lemma dim_adjoin_simple_eq_one_iff : dim F F⟮α⟯ = 1 ↔ α ∈ (⊥ : intermediate_field F E) :=
-by { rw [dim_adjoin_eq_one_iff], exact set.singleton_subset_iff }
+by { rw dim_adjoin_eq_one_iff, exact set.singleton_subset_iff }
 
 lemma findim_adjoin_eq_one_iff : findim F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
-by rw [←findim_intermediate_field_eq_findim_subalgebra, subalgebra.findim_eq_one_iff,
-      ←bot_to_subalgebra, to_subalgebra_eq_iff, adjoin_eq_bot_iff]
+iff.trans findim_eq_one_iff adjoin_eq_bot_iff
 
 lemma findim_adjoin_simple_eq_one_iff : findim F F⟮α⟯ = 1 ↔ α ∈ (⊥ : intermediate_field F E) :=
 by { rw [findim_adjoin_eq_one_iff], exact set.singleton_subset_iff }

src/field_theory/intermediate_field.lean

@@ -295,24 +295,35 @@ end tower
 
 section finite_dimensional
 
-instance finite_dimensional_left [finite_dimensional K L] (F : intermediate_field K L) :
-  finite_dimensional K F :=
+variables (F E : intermediate_field K L)
+
+instance finite_dimensional_left [finite_dimensional K L] : finite_dimensional K F :=
 finite_dimensional.finite_dimensional_submodule F.to_subalgebra.to_submodule
 
-instance finite_dimensional_right [finite_dimensional K L] (F : intermediate_field K L) :
-  finite_dimensional F L :=
+instance finite_dimensional_right [finite_dimensional K L] : finite_dimensional F L :=
 right K F L
 
-lemma eq_of_le_of_findim_le [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+@[simp] lemma dim_eq_dim_subalgebra :
+  vector_space.dim K F.to_subalgebra = vector_space.dim K F := rfl
+
+@[simp] lemma findim_eq_findim_subalgebra :
+  findim K F.to_subalgebra = findim K F := rfl
+
+variables {F} {E}
+
+@[simp] lemma to_subalgebra_eq_iff : F.to_subalgebra = E.to_subalgebra ↔ F = E :=
+by { rw [subalgebra.ext_iff, intermediate_field.ext'_iff, set.ext_iff], refl }
+
+lemma eq_of_le_of_findim_le [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim K E ≤ findim K F) : F = E :=
 intermediate_field.ext'_iff.mpr (submodule.ext'_iff.mp (eq_of_le_of_findim_le
   (show F.to_subalgebra.to_submodule ≤ E.to_subalgebra.to_submodule, by exact h_le) h_findim))
 
-lemma eq_of_le_of_findim_eq [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+lemma eq_of_le_of_findim_eq [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim K F = findim K E) : F = E :=
 eq_of_le_of_findim_le h_le h_findim.ge
 
-lemma eq_of_le_of_findim_le' [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+lemma eq_of_le_of_findim_le' [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim F L ≤ findim E L) : F = E :=
 begin
   apply eq_of_le_of_findim_le h_le,
@@ -322,7 +333,7 @@ begin
   nlinarith,
 end
 
-lemma eq_of_le_of_findim_eq' [finite_dimensional K L] {F E : intermediate_field K L} (h_le : F ≤ E)
+lemma eq_of_le_of_findim_eq' [finite_dimensional K L] (h_le : F ≤ E)
   (h_findim : findim F L = findim E L) : F = E :=
 eq_of_le_of_findim_le' h_le h_findim.le