Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-07-08 07:12 eb271b26

View on Github →

feat(data/int/basic): some lemmas (#3313) A few small lemmas about to_nat that I wanted while playing with exact sequences.

Estimated changes

added theorem int.le_add_one
added theorem int.to_nat_add
added theorem int.to_nat_add_one
added theorem int.to_nat_one
added theorem int.to_nat_zero