Commit 2026-10-03 10:16 e9b79b50

View on Github →

feat: generalize Polynomial.irreducible_comp (#42344) The new statement doesn't require the polynomials be monic. There's also an iff version.

Estimated changes

Modified Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean

modified theorem Polynomial.irreducible_comp

added theorem Polynomial.irreducible_comp_iff

Modified Mathlib/FieldTheory/KummerExtension.lean

added theorem norm_root_X_pow_sub_C