Commit 2025-12-12 18:47 12d559de

View on Github →

feat(Algebra/Order/Ring/Archimedean): ⊤ ≠ 0 (#32800) As well as some trivial drive-by golfing.

Estimated changes

modified theorem ArchimedeanClass.mk_natCast