Commit 2024-02-29 10:41 925c6abe
View on Github →feat: positivity extensions for Finset.card, Fintype.card (#10610)
Leverage the new proveFinsetNonempty prover to write a positivity extension about Finset.card. Also write the corresponding positivity extension for Fintype.card.
I put the two new extensions in a new file rather than Tactic.Positivity.Basic or Data.Fintype.Card because the former doesn't import any finiteness and the latter doesn't import linearly ordered fields. But I don't really mind where the extensions end up.
From LeanAPAP