feat(FieldTheory): implement Artin-Schreier theorem by kedlaya · Pull Request #41911 · leanprover-community/mathlib4

kedlaya · 2026-07-19T01:31:13Z

Implement the theorem of Artin-Schreier that a field with a finite algebraically closed extension is either algebraically closed or real closed. Depends on Artin-Schreier extensions of fields of characteristic p (#43947).

depends on: feat(FieldTheory): Artin-Schreier extensions of fields #43947

github-actions · 2026-07-19T01:31:21Z

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

github-actions · 2026-07-19T01:32:27Z

PR summary 2fecd40b78

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.FieldTheory.ArtinSchreierExtension` (new file)	2002
`Mathlib.FieldTheory.IsRealClosed.ArtinSchreier` (new file)	2740

Declarations diff (regex)

+ artinSchreierPoly_irreducible
+ artinSchreierPoly_irreducible_or_splits
+ artinSchreierPoly_isMonicOfDegree
+ artinSchreierPoly_splits
+ artinSchreierPoly_taylor
+ cyclic_charP_as_param
+ cyclic_charP_splitting
+ dvd_natDegree_of_monic_of_irreducible
+ exists_root_of_natDegree_eq_one
+ exists_root_or_all_irreducible_divisors
+ exists_root_or_all_irreducible_divisors'
+ irreducible_artinSchreierPoly_tower
+ irreducible_of_natDegree_eq_one
+ isAlgClosed_of_isSquare_neg_one
+ isAlgClosed_or_isRealClosed
+ isCyclic_charP_tfae
+ isRealClosed_of_isAlgClosed_adjoin
+ isSquare_mul_add_or_isSquare_neg
+ not_charP_of_finrank
+ perfect_of_finite_dimensional_algebraic_closure
+ prime_of_natDegree_eq_one

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 2fecd40).

+14 new declarations
−0 removed declarations

+IsAlgClosure.congr_simp
+Polynomial.dvd_natDegree_of_monic_of_irreducible
+Polynomial.exists_root_of_natDegree_eq_one
+Polynomial.irreducible_of_natDegree_eq_one
+Polynomial.prime_of_natDegree_eq_one
+artinSchreierPoly_irreducible
+artinSchreierPoly_irreducible_or_splits
+artinSchreierPoly_isMonicOfDegree
+artinSchreierPoly_splits
+artinSchreierPoly_taylor
+cyclic_charP_splitting
+irreducible_artinSchreierPoly_tower
+isAlgClosed_or_isRealClosed
+isCyclic_charP_tfae

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5074	1

Current commit 2fecd40b78
Reference commit 065356127b

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.py 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).

SnirBroshi · 2026-07-19T01:40:09Z

Hello, can you disclose any AI usage per the contribution guidelines (linked above)?

kedlaya · 2026-07-19T02:57:51Z

Hello, can you disclose any AI usage per the contribution guidelines (linked above)?

none

ScottCarnahan

These results would make a fine addition to mathlib. My main suggestion is to look over the mathlib naming conventions page.

ScottCarnahan · 2026-09-14T05:20:14Z

+/- If a field admits an algebraically closed extension of degree dividing a prime `p`, any
+   polynomial either has a root or has all irreducible divisors of degree `p` and degree
+   divisible by `p`. -/
+lemma divisor_by_finrank {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :


Suggested change

lemma divisor_by_finrank {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

lemma exists_root_or_all_irreducible_divisors {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

Feel free to use a name that you prefer, but it should reflect the statement of the lemma somehow.

I confess I find these naming conventions an utter mystery, so I mostly followed your suggestions.

ScottCarnahan · 2026-09-14T05:20:51Z

+   polynomial either has a root or has all irreducible divisors of degree `p` and degree
+   divisible by `p`. -/


Suggested change

polynomial either has a root or has all irreducible divisors of degree `p` and degree

divisible by `p`. -/

polynomial either has a root or has all irreducible divisors of degree `p`. -/

ScottCarnahan · 2026-09-14T05:21:36Z

+  have ⟨x, hx⟩ := exists_root_of_natDegree_eq_one h
+  exact ⟨x, hx.dvd h2⟩
+
+lemma divisor_by_finrank' {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :


Suggested change

lemma divisor_by_finrank' {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

lemma exists_root_or_all_irreducible_divisors' {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

ScottCarnahan · 2026-09-14T05:22:46Z

+    f (fun d _ h1 h2 ↦ (h d h1 h2).symm.dvd))
+
+/- A field admitting a finite extension which is algebraically closed is perfect. -/
+lemma finite_alg_closure_perfect [hf : FiniteDimensional F K] : PerfectField F := by


Suggested change

lemma finite_alg_closure_perfect [hf : FiniteDimensional F K] : PerfectField F := by

lemma perfect_of_finite_dimensional [hf : FiniteDimensional F K] : PerfectField F := by

ScottCarnahan · 2026-09-14T05:24:47Z

+
+/- If a field admits an extension of prime degree `p` which is algebraically closed, then
+   its characteristic cannot equal `p`. -/
+lemma finite_alg_closure_prime {p : ℕ} (hp : p.Prime) (hr : finrank F K = p) : ¬CharP F p := by


Suggested change

lemma finite_alg_closure_prime {p : ℕ} (hp : p.Prime) (hr : finrank F K = p) : ¬CharP F p := by

lemma not_charP_of_finrank {p : ℕ} (hp : p.Prime) (hr : finrank F K = p) : ¬CharP F p := by

ScottCarnahan · 2026-09-14T05:25:49Z

+
+/- If `a` and `b` belong to a field which admits an algebraically closed quadratic extension,
+   then one of `a^2 + b` or `-b` is a square. -/
+lemma quadratic_alg_closure (h : finrank F K ∣ 2) (a b : F) :


Suggested change

lemma quadratic_alg_closure (h : finrank F K ∣ 2) (a b : F) :

lemma isSquare_mul_add_or_isSquare_neg (h : finrank F K ∣ 2) (a b : F) :

ScottCarnahan · 2026-09-14T05:27:36Z

+
+/- A field containing a square root of `-1` and admitting a finite extension which is algebraically
+   closed is itself algebraically closed. -/
+lemma finite_alg_closure_i [hf : FiniteDimensional F K] (hm : IsSquare (-1 : F)) :


Suggested change

lemma finite_alg_closure_i [hf : FiniteDimensional F K] (hm : IsSquare (-1 : F)) :

lemma isAlgClosed_of_isSquare_neg_one [hf : FiniteDimensional F K] (hm : IsSquare (-1 : F)) :

ScottCarnahan · 2026-09-14T05:28:27Z

+/- A field in which `-1` is not a square, but adjoining its square root gives an algebraic
+   closure, is real closed. -/
+omit Hac in
+lemma RealClosed_from_quadratic (h1 : ¬IsSquare (-1 : F)) (h2 : ∃ i : K, i ^ 2 = -1 ∧


Suggested change

lemma RealClosed_from_quadratic (h1 : ¬IsSquare (-1 : F)) (h2 : ∃ i : K, i ^ 2 = -1 ∧

lemma isRealClosed_of_isAlgClosed_adjoin (h1 : ¬IsSquare (-1 : F)) (h2 : ∃ i : K, i ^ 2 = -1 ∧

ScottCarnahan · 2026-09-14T05:31:22Z

+  have h := irreducible_artinSchreierPoly_tower hp rfl a x ha
+  have h := (degree_eq_iff_natDegree_eq_of_pos one_pos).mp (Hac.degree_eq_one_of_irreducible K h)


Suggested change

have h := irreducible_artinSchreierPoly_tower hp rfl a x ha

have h := (degree_eq_iff_natDegree_eq_of_pos one_pos).mp (Hac.degree_eq_one_of_irreducible K h)

have h := (degree_eq_iff_natDegree_eq_of_pos one_pos).mp (Hac.degree_eq_one_of_irreducible K (irreducible_artinSchreierPoly_tower hp rfl a x ha)

ScottCarnahan · 2026-09-14T05:33:23Z

+  have hp1 := hp.one_lt
+  have := (Algebra.charP_iff F K p).mp ‹CharP F p›
+  have h := (artinSchreierPoly_irreducible_or_splits _).resolve_left h
+  have h_a {E} [Field E] (x : E) := artinSchreierPoly_isMonicOfDegree x hp1
+  have h_a1 := h_a ((algebraMap F K) a * x ^ (p-1))
+  have hs := (degree_eq_iff_natDegree_eq h_a1.ne_zero).mp.mt (h_a1.1.trans_ne hp.ne_zero)
+  have hy := eval_rootOfSplits h hs


I haven't tried golfing your proof, but it is unusual to need this many haves in succession.

They are all used but not all at once, I shuffled things around a bit in the last commit.

artie2000 · 2026-09-14T18:34:42Z

I've thought a bit about how to formalise this stuff in the past. I'll review shortly. One immediate comment is that I think this would be better as two PRs: one for Artin-Schreier extensions / classification and one for the link to ACFs/RCFs.

kedlaya · 2026-09-18T14:37:57Z

I've thought a bit about how to formalise this stuff in the past. I'll review shortly. One immediate comment is that I think this would be better as two PRs: one for Artin-Schreier extensions / classification and one for the link to ACFs/RCFs.

Fair enough, see #43947 for the former (which I'll make a dependency for this).

vihdzp · 2026-09-19T16:29:36Z

+
+# Artin-Schreier theorem
+
+This file proves the Artin-Schreier theorem `isAlgClosed_or_isRealClosed`:
+a field admitting a finite extension which is algebraically closed is either algebraically
+closed or real closed.
+


Suggested change

# Artin-Schreier theorem

This file proves the Artin-Schreier theorem `isAlgClosed_or_isRealClosed`:

a field admitting a finite extension which is algebraically closed is either algebraically

closed or real closed.

# Artin-Schreier theorem

This file proves the Artin-Schreier theorem `isAlgClosed_or_isRealClosed`:

a field admitting a finite extension which is algebraically closed is either algebraically

closed or real closed.

vihdzp · 2026-09-19T16:38:12Z

+
+/- The Artin-Schreier theorem: a field admitting a finite extension which is algebraically closed
+   is either algebraically closed or real closed. -/
+public theorem isAlgClosed_or_isRealClosed (F : Type u) (K : Type u) [Field F] [Field K]


We can have this version of the theorem, but I think this should itself be a corollary of the two theorems corresponding to each of the branches. If -1 is a square then F is algebraically closed; if -1 is not a square then F is real closed.

Also, is your proof is able to recover the fact that the extension is of degree 1 or 2 in the respective cases?

vihdzp · 2026-09-19T17:02:02Z

+    let n := exponent E K
+    rcases expChar_is_prime_or_one E p with h | h
+    · have : PerfectRing E p := by
+        refine ofSurjective E p (fun b ↦ ?_)


Suggested change

refine ofSurjective E p (fun b ↦ ?_)

refine ofSurjective E p fun b ↦ ?_

vihdzp · 2026-09-19T17:02:13Z

+    rcases expChar_is_prime_or_one E p with h | h
+    · have : PerfectRing E p := by
+        refine ofSurjective E p (fun b ↦ ?_)
+        obtain ⟨x, hx⟩ := Hac.exists_pow_nat_eq ((algebraMap E K) b) (expChar_pow_pos E p (n + 1))


Suggested change

obtain ⟨x, hx⟩ := Hac.exists_pow_nat_eq ((algebraMap E K) b) (expChar_pow_pos E p (n + 1))

obtain ⟨x, hx⟩ := Hac.exists_pow_nat_eq (algebraMap E K b) (expChar_pow_pos E p (n + 1))

vihdzp · 2026-09-19T17:02:42Z

+  have : PerfectField E := by
+    let n := exponent E K
+    rcases expChar_is_prime_or_one E p with h | h
+    · have : PerfectRing E p := by


I think it might be a bit clearer to start the proof with suffices PerfectRing E p from toPerfectField E p. Saves you the indent.

mathlib-dependent-issues · 2026-09-20T08:32:42Z

This PR/issue depends on:

feat(FieldTheory): Artin-Schreier extensions of fields #43947
By Dependent Issues (🤖). Happy coding!

Artin-Schreier extensions, Artin-Schreier theorem

c2940a1

github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jul 19, 2026

github-actions Bot added the t-algebra Algebra (groups, rings, fields, etc) label Jul 19, 2026

kedlaya added 2 commits July 18, 2026 19:17

Update Mathlib.lean to reflect new files

325ee1b

Add module docstring to ArtinSchreier.lean + a bugfix

69ee923

jcommelin reviewed Jul 19, 2026

View reviewed changes

Inlined lemma finrank_divides; added some backticks in docstrings

f319c73

ScottCarnahan reviewed Sep 14, 2026

View reviewed changes

kedlaya added 2 commits September 16, 2026 14:05

Merge branch 'master' into artin-schreier

7da8066

Apply naming convention to ArtinSchreior

2fecd40

kedlaya mentioned this pull request Sep 18, 2026

feat(FieldTheory): Artin-Schreier extensions of fields #43947

Open

vihdzp reviewed Sep 19, 2026

View reviewed changes

mathlib-dependent-issues Bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Sep 20, 2026

kedlaya changed the title ~~feat(FieldTheory): implement Artin-Schreier extensions, Artin-Schreier theorem~~ feat(FieldTheory): implement Artin-Schreier theorem Sep 20, 2026

	lemma divisor_by_finrank {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :
	lemma exists_root_or_all_irreducible_divisors {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

		polynomial either has a root or has all irreducible divisors of degree `p` and degree
		divisible by `p`. -/

	lemma divisor_by_finrank' {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :
	lemma exists_root_or_all_irreducible_divisors' {p : ℕ} (f : F[X]) (hr : finrank F K ∣ p) (hp : p.Prime) :

	lemma finite_alg_closure_perfect [hf : FiniteDimensional F K] : PerfectField F := by
	lemma perfect_of_finite_dimensional [hf : FiniteDimensional F K] : PerfectField F := by

	lemma finite_alg_closure_prime {p : ℕ} (hp : p.Prime) (hr : finrank F K = p) : ¬CharP F p := by
	lemma not_charP_of_finrank {p : ℕ} (hp : p.Prime) (hr : finrank F K = p) : ¬CharP F p := by

	lemma quadratic_alg_closure (h : finrank F K ∣ 2) (a b : F) :
	lemma isSquare_mul_add_or_isSquare_neg (h : finrank F K ∣ 2) (a b : F) :

	lemma finite_alg_closure_i [hf : FiniteDimensional F K] (hm : IsSquare (-1 : F)) :
	lemma isAlgClosed_of_isSquare_neg_one [hf : FiniteDimensional F K] (hm : IsSquare (-1 : F)) :

	lemma RealClosed_from_quadratic (h1 : ¬IsSquare (-1 : F)) (h2 : ∃ i : K, i ^ 2 = -1 ∧
	lemma isRealClosed_of_isAlgClosed_adjoin (h1 : ¬IsSquare (-1 : F)) (h2 : ∃ i : K, i ^ 2 = -1 ∧

		have h := irreducible_artinSchreierPoly_tower hp rfl a x ha
		have h := (degree_eq_iff_natDegree_eq_of_pos one_pos).mp (Hac.degree_eq_one_of_irreducible K h)

	refine ofSurjective E p (fun b ↦ ?_)
	refine ofSurjective E p fun b ↦ ?_

	obtain ⟨x, hx⟩ := Hac.exists_pow_nat_eq ((algebraMap E K) b) (expChar_pow_pos E p (n + 1))
	obtain ⟨x, hx⟩ := Hac.exists_pow_nat_eq (algebraMap E K b) (expChar_pow_pos E p (n + 1))

Conversation

kedlaya commented Jul 19, 2026 • edited by tb65536 Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Jul 19, 2026

Welcome new contributor!

Uh oh!

github-actions Bot commented Jul 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 2fecd40b78

Import changes for modified files

Declarations diff (regex)

Declarations diff (Lean)

Uh oh!

SnirBroshi commented Jul 19, 2026

Uh oh!

kedlaya commented Jul 19, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ScottCarnahan left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

artie2000 commented Sep 14, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

kedlaya commented Sep 18, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp Sep 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mathlib-dependent-issues Bot commented Sep 20, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

kedlaya commented Jul 19, 2026 •

edited by tb65536

Loading

github-actions Bot commented Jul 19, 2026 •

edited

Loading

artie2000 commented Sep 14, 2026 •

edited

Loading

vihdzp Sep 19, 2026 •

edited

Loading