Def Hyperreal.st

Modification history

2026-03-06 17:09

Mathlib/Analysis/Real/Hyperreal.lean

refactor: deprecate bespoke `Hyperreal` machinery (#33650) …

Deleted Hyperreal.st View on Github →

2026-01-23 10:44

Mathlib/Analysis/Real/Hyperreal.lean

feat(Analysis/Real/Hyperreal): more lemmas on `ω` and `ε` (#33649) …

Added Hyperreal.st View on Github →