Commit 2025-12-24 17:12 1c119a38

View on Github →

feat: more theorems on ArchimedeanClass.stdPart (#33048)

Estimated changes

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

added theorem ArchimedeanClass.mk_intCast_nonneg

added theorem ArchimedeanClass.mk_natCast_nonneg

added theorem ArchimedeanClass.mk_ofNat

added theorem ArchimedeanClass.mk_ratCast_nonneg

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

added theorem ArchimedeanClass.FiniteElement.mk_add_mk

modified theorem ArchimedeanClass.FiniteElement.mk_intCast

added theorem ArchimedeanClass.FiniteElement.mk_le_mk

added theorem ArchimedeanClass.FiniteElement.mk_lt_mk

added theorem ArchimedeanClass.FiniteElement.mk_mul_mk

modified theorem ArchimedeanClass.FiniteElement.mk_natCast

deleted theorem ArchimedeanClass.FiniteElement.mk_neg

modified theorem ArchimedeanClass.FiniteElement.mk_one

added theorem ArchimedeanClass.FiniteElement.mk_ratCast

added theorem ArchimedeanClass.FiniteElement.mk_sub_mk

modified theorem ArchimedeanClass.FiniteElement.mk_zero

added theorem ArchimedeanClass.FiniteElement.neg_mk

added theorem ArchimedeanClass.FiniteResidueField.mk_ratCast

modified theorem ArchimedeanClass.stdPart_add

added theorem ArchimedeanClass.stdPart_add_eq_left

added theorem ArchimedeanClass.stdPart_add_eq_right

added theorem ArchimedeanClass.stdPart_eq_zero

modified theorem ArchimedeanClass.stdPart_intCast

added theorem ArchimedeanClass.stdPart_monotoneOn

deleted theorem ArchimedeanClass.stdPart_of_mk_ne_zero

modified theorem ArchimedeanClass.stdPart_sub

added theorem ArchimedeanClass.stdPart_sub_eq_left

added theorem ArchimedeanClass.stdPart_sub_eq_right