Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-09 22:10 ceecc887

View on Github →

chore(algebra/ring/order): avoid import of data.set.intervals (#16869)

Estimated changes

Modified src/algebra/group_power/order.lean

Modified src/algebra/order/ring.lean

modified theorem strict_mono_on_mul_self