Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-10 18:58 0bba837e

View on Github →

chore(data/nat/factorial): use n + 1 instead of n.succ in nat.factorial_succ (#9645)

Estimated changes

Modified src/data/nat/choose/basic.lean

Modified src/data/nat/factorial/basic.lean

modified theorem nat.factorial_succ

Modified src/number_theory/liouville/liouville_constant.lean