Revision #3280 → #3811 · back to history
48aa8c795216| Field | From #3280 | To #3811 |
|---|---|---|
| mathlib.decl | Hyperreal.st | ArchimedeanClass.stdPart |
| mathlib.module | Mathlib.Analysis.Real.Hyperreal | Mathlib.Algebra.Order.Ring.StandardPart |
| note | The standard part on `ℝ*` is `Hyperreal.st : ℝ* → ℝ` (defined in `Mathlib.Analysis.Real.Hyperreal`). | The standard-part function on `ℝ*` is `ArchimedeanClass.stdPart` (the former `Hyperreal.st` has been renamed and generalized). |
c0d95f0ced47603302803307b6108847d399b1dcee861a1f