Theorem exists_lt_nsmul

Modification history

2024-08-27 00:13

Mathlib/Algebra/Order/Archimedean/Basic.lean

feat(Algebra/Order/Archimedean): multiplicativize Archimedean (#15589) …

Deleted exists_lt_nsmul View on Github →

2023-08-08 05:54

Mathlib/Algebra/Order/Archimedean.lean

feat(Algebra/GroupPower): weaken TC assumptions (#6389) …

Added exists_lt_nsmul View on Github →