Theorem WithZero.mulArchimedean_iff

Modification history

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