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!

Estimated changes