Commit 2022-02-10 17:14 45ab382c

chore(field_theory/galois): make intermediate_field.fixing_subgroup_equiv computable (#11938) This also golfs and generalizes some results to reuse infrastructure from elsewhere. In particular, this generalizes:

• intermediate_field.fixed_field to fixed_points.intermediate_field, where the latter matches the API of fixed_points.subfield
• intermediate_field.fixing_subgroup to fixing_subgroup and fixing_submonoid This removes open_locale classical in favor of ensuring the lemmas take in the necessary decidable / fintype arguments.