Theorem norm_root_X_pow_sub_C

Modification history

2026-10-03 10:16
Mathlib/FieldTheory/KummerExtension.lean
feat: generalize `Polynomial.irreducible_comp` (#42344) …
Added norm_root_X_pow_sub_CView on Github →