Zulip Chat Archive
Stream: mathlib4
Topic: hypernaturals
Alok Singh (Nov 29 2024 at 02:01):
I added basic hypernatural number definitions modeled off of Hyperreal.lean in https://github.com/alok/mathlib4/tree/hypernaturals
also adds a small change to FilterProduct.lean to allow deriving LinearOrderedSemiRing for N*
What is the next step towards a PR? This is very minimal so far.
Last updated: May 02 2025 at 03:31 UTC