Fixed field under a group action.
This is the basis of the Fundamental Theorem of Galois Theory.
Given a (finite) group
G that acts on a field
F, we define
fixed_points G F,
the subfield consisting of elements of
F fixed_points by every element of
This subfield is then normal and separable, and in addition (TODO) if
G acts faithfully on
findim (fixed_points G F) F = fintype.card G.
fixed_points G F, the subfield consisting of elements of
Ffixed_points by every element of
Gis a group that acts on
minpoly G F x is the minimal polynomial of
(x : F) over
fixed_points G F.
Embedding produced from a faithful action.
Bijection between G and algebra homomorphisms that fix the fixed points