chore(Data/Rat): move Float functions to separate file

leanprover-community / batteries

The "batteries included" extended library for the Lean programming language and theorem prover

Apache License 2.0

253 stars 105 forks source link

Closed jcommelin closed 2 weeks ago

jcommelin commented 2 weeks ago

This separates the algebraic bits from the (basically unverifiable) numerical bits.

leanprover-community-bot commented 2 weeks ago

Mathlib CI status (docs):

✅ Mathlib branch batteries-pr-testing-1035 has successfully built against this PR. (2024-11-12 03:59:46) View Log