Theorem Nat.descFactorial_one

Modification history

2023-11-17 11:02

Mathlib/Data/Nat/Factorial/Basic.lean

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

Modified Nat.descFactorial_one View on Github →

2022-12-16 12:16

Mathlib/Data/Nat/Factorial/Basic.lean

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

Added Nat.descFactorial_one View on Github →