Commit 2025-01-14 06:06 c083085d

View on Github →

refactor(FieldTheory/KummerExtension): Split off irreducibility of X ^ p - a (#20695) This PR splits of irreducibility of X ^ p - a from FieldTheory/KummerExtension since it has lighter imports and can be used to golf a proof in FieldTheory/Perfect.

Estimated changes