Theorem irreducible_X_pow_sub_C_iff_forall_prime_of_odd

Modification history

2026-10-29 16:29
Mathlib/FieldTheory/KummerExtension.lean
chore(FieldTheory/KummerPolynomial): rename theorems (#45461) …
Added irreducible_X_pow_sub_C_iff_forall_prime_of_oddView on Github →