Zulip Chat Archive
Stream: new members
Topic: rationals
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):
See data/rat.lean in the mathlib repository.
Last updated: May 02 2025 at 03:31 UTC