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