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

[plp127]

Prove the criterion for X ^ n - C a to be irreducible when n is not necessarily odd. This resolves a TODO.

---

• depends on: feat: generalize Polynomial.irreducible_comp #42344
• depends on: chore(FieldTheory/KummerExtension): rename theorems #42886

[github-actions]

PR summary 817abb88b4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ X_pow_sub_C_irreducible
+ X_pow_sub_C_irreducible_iff_forall_prime
+ X_pow_sub_C_irreducible_iff_of_prime_pow_of_ne_two
+ X_pow_sub_C_irreducible_of_prime_pow_of_ne_two
+ X_pow_two_pow_sub_C_irreducible
+ _root_.Polynomial.irreducible_comp_iff
+ compAlgEquiv
+ compAlgEquiv_of
+ compAlgEquiv_root
+ compAlgEquiv_symm_of_of
+ compAlgEquiv_symm_of_root
+ compAlgEquiv_symm_root

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 817abb8).

• +13 new declarations
• −0 removed declarations

+AdjoinRoot.compAlgEquiv
+AdjoinRoot.compAlgEquiv_of
+AdjoinRoot.compAlgEquiv_root
+AdjoinRoot.compAlgEquiv_symm_of_of
+AdjoinRoot.compAlgEquiv_symm_of_root
+AdjoinRoot.compAlgEquiv_symm_root
+AdjoinRoot.powerBasis.congr_simp
+Polynomial.irreducible_comp_iff
+X_pow_sub_C_irreducible
+X_pow_sub_C_irreducible_iff_forall_prime
+X_pow_sub_C_irreducible_iff_of_prime_pow_of_ne_two
+X_pow_sub_C_irreducible_of_prime_pow_of_ne_two
+X_pow_two_pow_sub_C_irreducible

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 817abb88b4
Reference commit 818f61df41

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat: generalize Polynomial.irreducible_comp #42344
• chore(FieldTheory/KummerExtension): rename theorems #42886
  By Dependent Issues (🤖). Happy coding!