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_denView on Github →