Mathlib Changelog
v4
Changelog
About
Github
Theorem
Hyperreal.infiniteNeg_iff
Modification history
2026-03-06 17:09
Mathlib/Analysis/Real/Hyperreal.lean
refactor: deprecate bespoke `Hyperreal` machinery (#33650) …
Added
Hyperreal.infiniteNeg_iff
View on Github →