commit: 8789e5621b05dc770401bc0532e57a8dabee31c5

[log]
author: Kim Morrison <477956+kim-em@users.noreply.github.com>

Sat Aug 30 18:54:12 2025 +1000
committer: GitHub <noreply@github.com>

Sat Aug 30 08:54:12 2025 +0000
tree: dc0cb7f8842ef24c47419f8d44ade57ff20c2958
parent: fbf096510d09468dea406d712cc374828b57c135 [diff]

feat: missing Nat.fold(Rev)_add lemmas (#10182)

This PR adds lemmas about `Nat.fold` and `Nat.foldRev` on sums, to match
the existing theorems about `dfold` and `dfoldRev`.

src/Init/Data/Nat/Fold.lean[diff]

1 file changed

tree: dc0cb7f8842ef24c47419f8d44ade57ff20c2958

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.