Commit 2023-01-16 19:17 2186d6f8

View on Github →

feat port: Data.Fintype.Pi (#1602)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Pi.lean

added theorem Finset.univ_pi_univ

added theorem Fintype.coe_piFinset

added theorem Fintype.mem_piFinset

added theorem Fintype.piFinset_disjoint_of_disjoint

added theorem Fintype.piFinset_empty

added theorem Fintype.piFinset_singleton

added theorem Fintype.piFinset_subset

added theorem Fintype.piFinset_subsingleton

added theorem Fintype.piFinset_univ