mathlib
e871be25
- feat(data/real/nnreal): floor_semiring instance (#12495)
Go
Login via GitHub
Home
Pricing
FAQ
Install
Login
via GitHub
Commit
View On
GitHub
Commit
4 years ago
feat(data/real/nnreal): floor_semiring instance (#12495) [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.60nat.2Eceil.60.20on.20.60nnreal.60.20.3F/near/274353230)
Author
eric-wieser
Parents
8d2ffb8f
Loading