mathlib

45ab382c - chore(field_theory/galois): make `intermediate_field.fixing_subgroup_equiv` computable (#11938)

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.