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.

Estimated changes