feat(field_theory/adjoin): add dim_bot, finrank_bot (#10964)

Added two simp lemmas, showing that the dimension and finrank respectively of bottom intermediate fields are 1. 

Co-authored-by: Sebastian-Monnet <54352341+Sebastian-Monnet@users.noreply.github.com>

src/field_theory/adjoin.lean

@@ -375,6 +375,12 @@ by rw [← to_subalgebra_eq_iff, ← dim_eq_dim_subalgebra,
 by rw [← to_subalgebra_eq_iff, ← finrank_eq_finrank_subalgebra,
   subalgebra.finrank_eq_one_iff, bot_to_subalgebra]
 
+@[simp] lemma dim_bot : module.rank F (⊥ : intermediate_field F E) = 1 :=
+by rw dim_eq_one_iff
+
+@[simp] lemma finrank_bot : finrank F (⊥ : intermediate_field F E) = 1 :=
+by rw finrank_eq_one_iff
+
 lemma dim_adjoin_eq_one_iff : module.rank F (adjoin F S) = 1 ↔ S ⊆ (⊥ : intermediate_field F E) :=
 iff.trans dim_eq_one_iff adjoin_eq_bot_iff