Mathlib v3 is deprecated. Go to Mathlib v4

Def fin.nat_add

Modification history

2020-12-07 20:04
src/data/fin.lean
refactor(data/fin): use `order_embedding` for many maps (#5251) …
Modified fin.nat_addView on Github →
2018-11-05 13:47
data/fin.lean
feat(ring_theory/matrix): add minor, sub_[left|right|up|down], sub_[left|right]_[up][down] (#389) …
Added fin.nat_addView on Github →
2018-10-17 13:50
data/fin.lean
chore(data/fin): use uniform names; restructure
Deleted fin.nat_addView on Github →
2018-10-05 02:18
data/fin.lean
Expand and contract fin (#387)
Added fin.nat_addView on Github →