Commit 2025-07-24 12:57 576e5e1f

View on Github →

feat(Data/Real): add embedding of archimedean groups into Real (#26114) This is part of https://github.com/leanprover-community/mathlib4/pull/25140, and is the special case of Hahn embedding theorem applied to archimedean group.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Data/Rat/Lemmas.lean

added theorem Rat.mkRat_add_mkRat_of_den

Created Mathlib/Data/Real/Embedding.lean

added def Archimedean.embedReal

added theorem Archimedean.embedRealFun_add

added theorem Archimedean.embedRealFun_strictMono

added theorem Archimedean.embedRealFun_zero

added theorem Archimedean.embedReal_apply

added theorem Archimedean.embedReal_injective

added theorem Archimedean.embedReal_one

added theorem Archimedean.exists_orderAddMonoidHom_real_injective

added theorem Archimedean.mkRat_mem_ratLt

added theorem Archimedean.ratLt'_add

added theorem Archimedean.ratLt'_bddAbove

added theorem Archimedean.ratLt'_nonempty

added theorem Archimedean.ratLt_add

added theorem Archimedean.ratLt_bddAbove

added theorem Archimedean.ratLt_nonempty

added theorem mul_smul_one_lt_iff

added theorem num_le_nat_mul_den

added theorem num_smul_one_lt_den_smul_add