Theorem Int.succ_coe_nat_pos

Modification history

2024-04-03 11:58

Mathlib/Data/Int/Lemmas.lean

chore(Data/Int): Rename `coe_nat` to `natCast` (#11637) …

Deleted Int.succ_coe_nat_pos View on Github →

2023-01-02 18:09

Mathlib/Data/Int/Lemmas.lean

feat: port data.int.lemmas (#1271) …

Added Int.succ_coe_nat_pos View on Github →