Mathlib Changelog
v4
Changelog
About
Github
Theorem
Hyperreal.archimedeanClassMk_coe
Modification history
2026-09-26 18:40
Mathlib/Analysis/Real/Hyperreal.lean
chore: fix misspellings in declaration names (#44049) …
Added
Hyperreal.archimedeanClassMk_coe
View on Github →