Theorem Int.coe_nat_strictMono

Modification history

2024-05-28 07:17
Mathlib/Algebra/Order/Group/Int.lean
chore: Rename more `coe_nat`/`coe_int` to `natCast`/`intCast` (#13205)
Deleted Int.coe_nat_strictMonoView on Github →
2024-05-25 12:18
Mathlib/Algebra/Group/Int.lean
chore: move Int.coe_nat_strictMono (#13197)
Modified Int.coe_nat_strictMonoView on Github →
2022-11-22 07:59
Mathlib/Data/Int/Basic.lean
feat: add `fun x ↦ t` syntax (#617)
Modified Int.coe_nat_strictMonoView on Github →
2022-11-14 10:32
Mathlib/Data/Int/Basic.lean
feat: port data.int.basic (#584) …
Added Int.coe_nat_strictMonoView on Github →