Commit 2024-07-09 16:27 579a86ce
View on Github →feat(Fintype.Basic): Add two theorems supporting Auction Theory formalizations (#14163)
This PR adds two missing theorems in Mathlib.Data.Fintype.Basic, which is in asisstant of the other PR of mine formalized some basic theorems in GameTheory.AuctionTheory.Basic .
One may check the previous PR for Auction Theory here: #13248
I would sincerely appreciate a timely review of this PR, as I am eager to complete my first project on Auction Theory before my upcoming birthday. Thank you very much for your consideration and support!