Commit 2020-12-05 20:21 ae99c76d

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