Commit 2025-02-26 06:07 de459bf8

View on Github →

feat(Order/Archimedean): WithZero.mulArchimedean_iff (#22294) with the basic instance of WithZero.instMulArchimedean in an earlier file Now, #synth MulArchimedean ℤₘ₀ works

Estimated changes

Modified Mathlib/Algebra/Order/Archimedean/Basic.lean

Modified Mathlib/GroupTheory/ArchimedeanDensely.lean

added theorem OrderMonoidIso.mulArchimedean

added theorem WithZero.mulArchimedean_iff