Skip to content

feat(FieldTheory/KummerExtension): criterion for X ^ n - C a to be irreducible for even n - #42923

Open
plp127 wants to merge 31 commits into
leanprover-community:masterfrom
plp127:aliu/even-kummer
Open

feat(FieldTheory/KummerExtension): criterion for X ^ n - C a to be irreducible for even n#42923
plp127 wants to merge 31 commits into
leanprover-community:masterfrom
plp127:aliu/even-kummer

split proof

817abb8
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
post-or-update-summary-comment
succeeded Aug 19, 2026 in 1m 34s