Mathlib v3 is deprecated. Go to Mathlib v4

Theorem nat.desc_fac_of_sub

Modification history

2021-06-27 15:45

src/data/nat/factorial.lean

feat(data/nat/factorial): descending factorial (#7759) …

Deleted nat.desc_fac_of_sub View on Github →

2021-05-21 11:28

src/data/nat/factorial.lean

feat(data/fintype/card_embedding): the birthday problem (#7363)

Added nat.desc_fac_of_sub View on Github →