Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.succ_eq_one_add

Modification history

2021-08-04 07:05
src/algebra/ordered_ring.lean
refactor(nat/basic): Move lemma about nat (#8539)
Modified nat.succ_eq_one_addView on Github →
2021-06-01 23:18
src/algebra/group/hom_instances.lean
chore(data/nat): split out data/nat/pow (#7758) …
Modified nat.succ_eq_one_addView on Github →
2021-04-15 20:50
src/algebra/group/hom_instances.lean
chore(group/ring_hom): fix a nat nsmul diamond (#7201) …
Modified nat.succ_eq_one_addView on Github →
2021-04-14 08:29
src/data/nat/basic.lean
refactor(*): kill nat multiplication diamonds (#7084) …
Added nat.succ_eq_one_addView on Github →