commit: 1cf71e54cf268e87cf5c43c830d953f5c88e6c39

[log]
author: Markus Schmaus <markus.schmaus.math@gmail.com>

Mon Jun 17 07:35:32 2024 +0200
committer: GitHub <noreply@github.com>

Mon Jun 17 05:35:32 2024 +0000
tree: c5f2221e4bf4895acc2221ee2903252e14f81bd8
parent: 2efcbfe80360c66db451571a608930e115ee763e [diff]

feat: add missing theorems for `+ 1` and `- 1` normal form (#4242)

`Nat.succ_eq_add_one` and `Nat.pred_eq_sub_one` are now simp lemmas. For
theorems about `Nat.succ` or `Nat.pred` without corresponding theorem
for `+ 1` or `- 1`, this adds the corresponding theorem.

10 files changed

tree: c5f2221e4bf4895acc2221ee2903252e14f81bd8

README.md

This is the repository for Lean 4.

About

Installation

See Setting Up Lean.

Contributing

Please read our Contribution Guidelines first.

Building from Source

See Building Lean (documentation source: doc/make/index.md).