[Merged by Bors] - feat: standard part in non-Archimedean field

[vihdzp]

We define ArchimedeanClass.stdPart x as the unique real number with an infinitesimal difference from x. This generalizes Hyperreal.st for a general (non-)archimedean field.

---

• depends on: [Merged by Bors] - feat: alternate characterization of ≤ on Archimedean classes #29611
• depends on: [Merged by Bors] - feat: theorems on MulArchimedeanClass.mk (a / b) #29685
• depends on: [Merged by Bors] - feat: order instances on quotients #29735
• depends on: [Merged by Bors] - feat: f r = r for f : ℝ →+* ℝ #30486
• depends on: [Merged by Bors] - chore: generalize Subring.toIsOrderedRing to SubringClass #32212

[github-actions]

PR summary 89423f926a

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Algebra.Order.Ring.StandardPart (new file)	1349

---

Declarations diff

+ FiniteElement
+ FiniteResidueField
+ ext
+ ind
+ instLinearOrder
+ instance : Archimedean (FiniteResidueField K)
+ instance : CommRing (FiniteElement K) := by
+ instance : Field (FiniteResidueField K)
+ instance : IsDomain (FiniteElement K) := by
+ instance : IsOrderedRing (FiniteResidueField K)
+ instance : IsStrictOrderedRing (FiniteElement K) := by
+ instance : LinearOrder (FiniteElement K) := by
+ instance : LinearOrder (FiniteResidueField K)
+ instance : ValuationRing (FiniteElement K) := by
+ isUnit_iff_mk_eq_zero
+ lt_of_mk_lt_mk
+ mk_eq_mk
+ mk_eq_zero
+ mk_intCast
+ mk_le_add_mk_of_archimedean
+ mk_le_mk
+ mk_le_mk_add_of_archimedean
+ mk_lt_mk
+ mk_map_nonneg_of_archimedean
+ mk_natCast
+ mk_ne_zero
+ mk_neg
+ mk_one
+ mk_sub_pos_iff
+ mk_sub_stdPart_pos
+ mk_zero
+ not_isUnit_iff_mk_pos
+ ofArchimedean
+ ofArchimedean_apply
+ ofArchimedean_inj
+ ofArchimedean_injective
+ ofArchimedean_stdPart
+ ordConnected_preimage_mk
+ stdPart
+ stdPart_add
+ stdPart_div
+ stdPart_intCast
+ stdPart_inv
+ stdPart_mul
+ stdPart_natCast
+ stdPart_neg
+ stdPart_ofNat
+ stdPart_of_mk_ne_zero
+ stdPart_of_mk_nonneg
+ stdPart_one
+ stdPart_ratCast
+ stdPart_real
+ stdPart_sub
+ stdPart_zero
+ val_add
+ val_mul
+ val_one
+ val_sub
+ val_zero
++ mk
- instance [DecidableRel (· ≈ · : α → α → Prop)] : LinearOrder (Quotient s)

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

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.

[YaelDillies]

Thanks! 🚀

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

[jcommelin]

Can you add that as a lemma characterizing this def?

[vihdzp]

I had that on a follow-up PR, but I can move it here.

[vihdzp]

Just added this theorem, along with some prerequisite lemmas.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build
• Post-Build Step