Theorem OrderMonoidIso.mulArchimedean

Modification history

2025-04-10 16:38
Mathlib/GroupTheory/ArchimedeanDensely.lean
chore: deprecate semibundled ordered algebraic typeclasses (#20676) …
Modified OrderMonoidIso.mulArchimedeanView on Github →
2025-02-26 06:07
Mathlib/GroupTheory/ArchimedeanDensely.lean
feat(Order/Archimedean): `WithZero.mulArchimedean_iff` (#22294) …
Added OrderMonoidIso.mulArchimedeanView on Github →