Theorem Hyperreal.infinitesimal_iff

Modification history

2026-03-06 17:09
Mathlib/Analysis/Real/Hyperreal.lean
refactor: deprecate bespoke `Hyperreal` machinery (#33650) …
Added Hyperreal.infinitesimal_iffView on Github →