Commit 2025-12-19 07:43 477597f0

View on Github →

chore: replace unnecessary Fintype hypotheses with Finite (#33068) This PR fixes all of the violations of the unusedFintypeInType linter (#31794), preparing us for merging that linter and turning it on. Note: some files see rearrangements of declarations to enable cleaner sectioning between Fintype and Finite, but we generally try to stay close to the original style.

Estimated changes

modified theorem hasFDerivAt_finset_prod
modified theorem hasFDerivAt_list_prod'
modified theorem hasFDerivAt_multiset_prod
modified theorem hasStrictFDerivAt_list_prod
modified theorem PiLp.isUniformInducing_toLp