Theorem Int.sign_coe_nat_of_nonzero

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_nat_of_nonzero View on Github →

2024-01-06 09:51

Mathlib/Data/Int/Basic.lean

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

Modified Int.sign_coe_nat_of_nonzero View on Github →

2022-11-14 10:32

Mathlib/Data/Int/Basic.lean

feat: port data.int.basic (#584) …

Added Int.sign_coe_nat_of_nonzero View on Github →