Commit 2025-12-17 10:18 144fc71c

View on Github →

feat: standard part in non-Archimedean field (#29687) 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.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Order/Ring/Archimedean.lean

added theorem ArchimedeanClass.mk_le_add_mk_of_archimedean

added theorem ArchimedeanClass.mk_le_mk_add_of_archimedean

added theorem ArchimedeanClass.mk_map_nonneg_of_archimedean

Created Mathlib/Algebra/Order/Ring/StandardPart.lean

added theorem ArchimedeanClass.FiniteElement.ext

added theorem ArchimedeanClass.FiniteElement.isUnit_iff_mk_eq_zero

added theorem ArchimedeanClass.FiniteElement.mk_intCast

added theorem ArchimedeanClass.FiniteElement.mk_natCast

added theorem ArchimedeanClass.FiniteElement.mk_neg

added theorem ArchimedeanClass.FiniteElement.mk_one

added theorem ArchimedeanClass.FiniteElement.mk_zero

added theorem ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos

added theorem ArchimedeanClass.FiniteElement.val_add

added theorem ArchimedeanClass.FiniteElement.val_mul

added theorem ArchimedeanClass.FiniteElement.val_one

added theorem ArchimedeanClass.FiniteElement.val_sub

added theorem ArchimedeanClass.FiniteElement.val_zero

added theorem ArchimedeanClass.FiniteResidueField.ind

added theorem ArchimedeanClass.FiniteResidueField.lt_of_mk_lt_mk

added def ArchimedeanClass.FiniteResidueField.mk

added theorem ArchimedeanClass.FiniteResidueField.mk_eq_mk

added theorem ArchimedeanClass.FiniteResidueField.mk_eq_zero

added theorem ArchimedeanClass.FiniteResidueField.mk_le_mk

added theorem ArchimedeanClass.FiniteResidueField.mk_lt_mk

added theorem ArchimedeanClass.FiniteResidueField.mk_ne_zero

added def ArchimedeanClass.FiniteResidueField.ofArchimedean

added theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_apply

added theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_inj

added theorem ArchimedeanClass.FiniteResidueField.ofArchimedean_injective

added def ArchimedeanClass.FiniteResidueField

added theorem ArchimedeanClass.mk_sub_pos_iff

added theorem ArchimedeanClass.mk_sub_stdPart_pos

added theorem ArchimedeanClass.ofArchimedean_stdPart

added theorem ArchimedeanClass.stdPart_add

added theorem ArchimedeanClass.stdPart_div

added theorem ArchimedeanClass.stdPart_intCast

added theorem ArchimedeanClass.stdPart_inv

added theorem ArchimedeanClass.stdPart_mul

added theorem ArchimedeanClass.stdPart_natCast

added theorem ArchimedeanClass.stdPart_neg

added theorem ArchimedeanClass.stdPart_ofNat

added theorem ArchimedeanClass.stdPart_of_mk_ne_zero

added theorem ArchimedeanClass.stdPart_of_mk_nonneg

added theorem ArchimedeanClass.stdPart_one

added theorem ArchimedeanClass.stdPart_ratCast

added theorem ArchimedeanClass.stdPart_real

added theorem ArchimedeanClass.stdPart_sub

added theorem ArchimedeanClass.stdPart_zero

Modified Mathlib/Order/Quotient.lean