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
.