mathlib

03c302dc - feat(field_theory/fixed): field is separable over fixed subfield under group action (#3568)