Commit 2025-09-13 12:46 0a26ae31

View on Github →

feat: archimedean classes of rationals (#28187) We prove some lemmas relating ArchimedeanClass to ℚ and other archimedean fields.

Estimated changes

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

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

added theorem ArchimedeanClass.eq_zero_or_top_of_archimedean

added theorem ArchimedeanClass.mk_eq_zero_of_archimedean

added theorem ArchimedeanClass.mk_intCast

added theorem ArchimedeanClass.mk_map_of_archimedean'

added theorem ArchimedeanClass.mk_map_of_archimedean

added theorem ArchimedeanClass.mk_natCast

added theorem ArchimedeanClass.mk_ratCast

added theorem ArchimedeanClass.orderHom_zero

Modified Mathlib/Order/Antisymmetrization.lean