Theorem ArchimedeanClass.isAddRegular_mk

Modification history

2026-01-08 11:26
Mathlib/Algebra/Order/Ring/Archimedean.lean
refactor: make `LinearOrderedCommMonoidWithZero`s cancellative (#31749) …
Added ArchimedeanClass.isAddRegular_mkView on Github →