Mathlib Changelog
v4
Changelog
About
Github
Theorem
ArchimedeanClass.mk_intCast_nonneg
Modification history
2025-12-24 17:12
Mathlib/Algebra/Order/Ring/Archimedean.lean
feat: more theorems on `ArchimedeanClass.stdPart` (#33048)
Added
ArchimedeanClass.mk_intCast_nonneg
View on Github →