feat(FieldTheory): real closed field #33697

artie2000 · 2026-01-07T02:01:26Z

Define real closed fields
Prove some very basic properties

github-actions · 2026-01-07T02:02:34Z

PR summary 8520ad2c07

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.FieldTheory.IsRealClosed.Basic` (new file)	786

Declarations diff

+ IsRealClosed
+ _root_.IsSquare.of_not_isSquare_neg
+ exists_eq_pow_of_isSquare
+ exists_eq_pow_of_nonneg
+ exists_eq_pow_of_odd
+ exists_eq_zpow_of_isSquare
+ exists_eq_zpow_of_nonneg
+ exists_eq_zpow_of_odd
+ isSquare_neg_of_not_isSquare
+ nonneg_iff_isSquare
+ of_linearOrderedField

You can run this locally as follows

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

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/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/FieldTheory/IsRealClosed/Basic.lean

vihdzp · 2026-01-07T04:13:32Z

Mathlib/FieldTheory/IsRealClosed/Basic.lean

+open Polynomial
+
+/-- A field `R` is real closed if
+    1. `R` is real


Don't you mean?

Suggested change

1. `R` is real

1. `R` is semireal

"(Formally) real" and "semireal" are equivalent for a field, and so nobody ever distinguishes them. I've used IsSemireal as the preferred spelling because it's the usual definition of a "real field."

Do we have a definition for real fields in Mathlib, though? I'd rather keep the wording clear.

It's coming very soon!
You're allowed to lie a little about the implementation if it makes it clearer what you mean mathematically
And here it's not even lying imo

Mathlib/FieldTheory/IsRealClosed/Basic.lean

vihdzp · 2026-01-07T04:18:13Z

Mathlib/FieldTheory/IsRealClosed/Basic.lean

+-/
+class IsRealClosed (R : Type*) [Field R] : Prop extends IsSemireal R where
+  isSquare_or_isSquare_neg (x : R) : IsSquare x ∨ IsSquare (-x)
+  exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x


Do you think this might save us some tedium in the future?

Suggested change

exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x

exists_isRoot_of_odd_natDegree' {f : R[X]} (hf : Odd f.natDegree) (hf' : 1 < f.degree) : ∃ x, f.IsRoot x

You can then prove the version without the extra hypothesis as a theorem (every linear polynomial has a root).

I fear I have already done the tedious work you mention haha
I like this idea (and you can do a similar thing where you turn the first condition into an implication), but I'm not sure it should be the definition? I can make it an alternate constructor?

If you don't need this hypothesis, it's as easy as putting a single underscore in your proof. Having a new constructor would also mean we couldn't use where notation on it.

The where notation thing is true
But idk, feels weird to me to change the definition like this

Yeah OK just checked my project and this is a three line tactic proof making use of a utility lemma that isn't in Mathlib yet. The polynomial library sucks enough that I don't want to add something like this. I can add the alternate constructor in a future PR though?

Maybe an alternate solution is to just add the lemma "every polynomial of degree 1 has a root" to Mathlib?

My bad, we have it already: Polynomial.exists_root_of_degree_eq_one. Polynomial library doesn't suck!
But I thought about it and adding this condition wouldn't actually help? Like, any proof that works for degree > 1 is going to work for degree = 1. In fact it's usually going to be by induction, and degree = 1 is the base case so you can't avoid it.
What I do want to add is the theorem that, if all nonlinear odd-degree polynomials are reducible, then they all have roots (Polynomial.has_root_of_odd_natDegree_imp_not_irreducible in my repo). That's the real way to kill the base case imo.

Alright then! No need to bother with this, then.

Mathlib/FieldTheory/IsRealClosed/Basic.lean

vihdzp · 2026-01-07T04:20:30Z

Mathlib/FieldTheory/IsRealClosed/Basic.lean

+
+variable {R : Type u} [Field R]
+
+theorem of_orderedField [LinearOrder R] [IsStrictOrderedRing R]


Suggested change

theorem of_orderedField [LinearOrder R] [IsStrictOrderedRing R]

theorem of_orderedField [LinearOrder R] [IsOrderedRing R]

And maybe this could be of_isOrderedRing?

As discussed on Zulip, [Field F] [LinearOrder F] [IsStrictOrderedRing F] is the preferred spelling of "ordered field" for performance reasons.

And I like the idea of using LinearOrderedField as an abbreviation in names for [Field F] [LinearOrder F] [IsStrictOrderedRing F]. It's used throughout the library as a result of renames not happening when unbundling occured. Maybe it should be documented somewhere?

(I should change to of_linearOrderedField though, thanks for pointing out)

Mathlib/FieldTheory/IsRealClosed/Basic.lean

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

Mathlib/FieldTheory/IsRealClosed/Basic.lean

vihdzp · 2026-01-07T23:39:59Z

Mathlib/FieldTheory/IsRealClosed/Basic.lean

 variable [IsRealClosed R]

+@[aesop 50%]
+theorem _root_.IsSquare.of_not_isSquare_neg {x : R} (hx : ¬ IsSquare (-x)) : IsSquare x := by aesop


This is an iff for x ≠ 0, might that be worth adding too? And perhaps we could have ¬ IsSquare x → IsSquare (-x) as well?

The iff needs semireal implies formally real (or similar) so I'll defer it until I've upstreamed formally real rings

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

…rcf_def

initial commit

4eaca05

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Jan 7, 2026

artie2000 added 3 commits January 7, 2026 02:18

fix

d2b7f9f

module

37dca03

expose public section

e2c4eaf

artie2000 changed the title ~~feat(FieldTheory): Real Closed Field~~ feat(FieldTheory): real closed field Jan 7, 2026

vihdzp reviewed Jan 7, 2026

View reviewed changes

Update Mathlib/FieldTheory/IsRealClosed/Basic.lean

4bb2378

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

artie2000 added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 7, 2026

artie2000 and others added 4 commits January 7, 2026 17:35

Update Mathlib/FieldTheory/IsRealClosed/Basic.lean

5214382

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

review suggestions

a458940

fix name

3ffc739

add zpow versions

1f1b3e9

vihdzp approved these changes Jan 7, 2026

View reviewed changes

Mathlib/FieldTheory/IsRealClosed/Basic.lean Outdated Show resolved Hide resolved

add util lemma

9b7ed81

vihdzp reviewed Jan 7, 2026

View reviewed changes

artie2000 and others added 3 commits January 8, 2026 00:08

Update Mathlib/FieldTheory/IsRealClosed/Basic.lean

7db148a

Co-authored-by: Violeta Hernández Palacios <vi.hdz.p@gmail.com>

add lemma

4aade12

Merge branch 'rcf_def' of https://github.com/artie2000/mathlib4 into …

86634b2

…rcf_def

artie2000 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 8, 2026

	exists_isRoot_of_odd_natDegree {f : R[X]} (hf : Odd f.natDegree) : ∃ x, f.IsRoot x
	exists_isRoot_of_odd_natDegree' {f : R[X]} (hf : Odd f.natDegree) (hf' : 1 < f.degree) : ∃ x, f.IsRoot x


		variable {R : Type u} [Field R]

		theorem of_orderedField [LinearOrder R] [IsStrictOrderedRing R]

feat(FieldTheory): real closed field #33697

Are you sure you want to change the base?

feat(FieldTheory): real closed field #33697

Conversation

artie2000 commented Jan 7, 2026

Uh oh!

github-actions bot commented Jan 7, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 8520ad2c07

Import changes for modified files

Declarations diff

Uh oh!

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

artie2000 Jan 7, 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!

artie2000 Jan 7, 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!

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!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

vihdzp Jan 7, 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!

artie2000 Jan 8, 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!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

github-actions bot commented Jan 7, 2026 •

edited

Loading

artie2000 Jan 7, 2026 •

edited

Loading

artie2000 Jan 7, 2026 •

edited

Loading

vihdzp Jan 7, 2026 •

edited

Loading

artie2000 Jan 8, 2026 •

edited

Loading