Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-27 15:45 f8e9c179

View on Github →

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

  • rename desc_fac to asc_factorial
  • define desc_factorial
  • update data.fintype.card_embedding to use desc_factorial

Estimated changes

deleted theorem fintype.card_embedding
added theorem nat.asc_factorial_pos
added theorem nat.asc_factorial_succ
added theorem nat.asc_factorial_zero
deleted def nat.desc_fac
deleted theorem nat.desc_fac_eq_div
deleted theorem nat.desc_fac_of_sub
deleted theorem nat.desc_fac_succ
deleted theorem nat.desc_fac_zero
added theorem nat.desc_factorial_one
modified def nat.factorial
modified theorem nat.factorial_inj
modified theorem nat.factorial_lt
added theorem nat.succ_asc_factorial
deleted theorem nat.succ_desc_fac
added theorem nat.zero_asc_factorial
deleted theorem nat.zero_desc_fac