Commit 2023-01-19 17:01 6af22406

View on Github →

feat: port Data.Fintype.Prod (#1676)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Prod.lean

added theorem Finset.univ_product_univ

added theorem Fintype.card_prod

added theorem Pi.infinite_of_exists_right

added theorem Set.toFinset_off_diag

added theorem Set.toFinset_prod

added theorem infinite_prod