feat(field_theory/galois): Is_galois iff is_galois bot (#5231)
Proves that E/F is Galois iff E/bot is Galois.
This is useful in Galois theory because it gives a new way of showing that E/F is Galois:
1) Show that bot is the fixed field of some subgroup
2) Apply `is_galois.of_fixed_field`
3) Apply `is_galois_iff_is_galois_bot`
More to be added later (once #5225 is merged): Galois is preserved by alg_equiv, is_galois_iff_galois_top
Co-authored-by: tb65536 <tb65536@users.noreply.github.com>
