Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-08-04 07:05 292e3fa1

View on Github →

refactor(nat/basic): Move lemma about nat (#8539)

Estimated changes

Modified src/algebra/group/hom_instances.lean

Modified src/algebra/ordered_ring.lean

deleted theorem nat.succ_eq_one_add

Modified src/data/nat/basic.lean

added theorem nat.succ_eq_one_add