Commit 2024-05-25 12:18 dacd3b14

View on Github →

chore: move Int.coe_nat_strictMono (#13197)

Estimated changes

Modified Mathlib/Algebra/Group/Int.lean

deleted theorem Int.coe_nat_strictMono

Modified Mathlib/Algebra/GroupPower/IterateHom.lean

Modified Mathlib/Algebra/Order/Group/Int.lean

added theorem Int.coe_nat_strictMono