Theorem Nat.ascFactorial_succ

Modification history

2024-01-09 10:40

Mathlib/Data/Nat/Factorial/Basic.lean

chore: shift Nat.ascFactorial down by one (#7965) …

Modified Nat.ascFactorial_succ View on Github →

2023-11-17 11:02

Mathlib/Data/Nat/Factorial/Basic.lean

fix: some cleanup in `Nat.Factorial.Basic` (#8422) …

Modified Nat.ascFactorial_succ View on Github →

2022-12-16 12:16

Mathlib/Data/Nat/Factorial/Basic.lean

feat: Port `Data.Nat.Factorial.Basic` (#1066) …

Added Nat.ascFactorial_succ View on Github →