Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-04 21:07 c7d7d833

View on Github →

chore(data/nat): use notation n!, minor golf (#7032)

Estimated changes

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

modified theorem nat.add_choose

added theorem nat.add_choose_mul_factorial_mul_factorial

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

modified theorem add_pow

modified theorem commute.add_pow

Modified src/data/nat/factorial.lean

modified theorem nat.factorial_le