Commit 2023-10-27 13:10 a6c4c7e8

View on Github →

feat: Fintype.prod_prod_type (#7955)

Estimated changes

Modified Mathlib/Data/Fintype/BigOperators.lean

added theorem Fintype.prod_prod_type'

added theorem Fintype.prod_prod_type

added theorem Fintype.prod_prod_type_right'

added theorem Fintype.prod_prod_type_right