Theorem Num.to_nat_inj

Modification history

2023-11-09 00:36

Mathlib/Data/Num/Lemmas.lean

chore: Merge back ordered cancellative stuff (#8170) …

Modified Num.to_nat_inj View on Github →

2023-04-10 15:18

Mathlib/Data/Num/Lemmas.lean

feat: port Data.Num.Lemmas (#2784)

Added Num.to_nat_inj View on Github →