Stream: new members
garySebastian (Oct 21 2018 at 20:38):
Is there a lean module for working with rational numbers? There are some messages here about a type 'rat'/ℚ, but the lean repository doesn't show anything.
Bryan Gin-ge Chen (Oct 21 2018 at 20:39):
data/rat.lean in the mathlib repository.
Last updated: May 14 2021 at 23:14 UTC