Mathlib Changelog
v4
Changelog
About
Github
Theorem
Rat.mkRat_add_mkRat_of_den
Modification history
2025-07-24 12:57
Mathlib/Data/Rat/Lemmas.lean
feat(Data/Real): add embedding of archimedean groups into Real (#26114) …
Added
Rat.mkRat_add_mkRat_of_den
View on Github →