Commit 2024-03-12 10:00 3c029be9
View on Github →feat: cons lemmas for Finset.noncommProd (#11194)
These are more general than the insert versions as they do not assume DecidableEq.
This also lets some later proofs be golfed.
feat: cons lemmas for Finset.noncommProd (#11194)
These are more general than the insert versions as they do not assume DecidableEq.
This also lets some later proofs be golfed.