Commit 2024-10-23 21:11 5b9d3428
View on Github →feat(FieldTheory/Fixed): Finite group surjects onto automorphisms fixing the fixed field (#18143)
This PR shows that if a finite group G acts on a field F, then G surjects onto F ≃ₐ[FixedPoints.subfield G F] F. We already have this result in the case that G acts faithfully, so for the general case it's just a matter of quotienting by the kernel of the action.