Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-30 10:46 37212a78

View on Github →

feat(data/fin*): uniqueness of increasing bijection (#2258)

  • feat(data/fin*): uniqueness of increasing bijection
  • protect
  • remove tidy call
  • Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/data/finset.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • Update src/data/fintype/card.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com
  • prove prod_add, and use this to prove sum_pow_mul_eq_add_pow
  • forgot to save
  • fix build
  • remove card_sub_card

Estimated changes