Theorem Int.sign_coe_add_one

Modification history

2024-04-03 11:58

Mathlib/Data/Int/Defs.lean

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

Deleted Int.sign_coe_add_one View on Github →

2024-01-06 09:51

Mathlib/Data/Int/Basic.lean

refactor: Split off basic `Int` file (#9443) …

Modified Int.sign_coe_add_one View on Github →

2023-03-29 01:18

Mathlib/Data/Int/Basic.lean

feat: port IMO 2006 Q5 helper results (#3136) …

Added Int.sign_coe_add_one View on Github →