Commit 2023-01-16 18:31 2c7f9c6b

View on Github →

feat: port Data.Finset.Prod (#1599)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Prod.lean

added theorem Finset.Nonempty.fst

added theorem Finset.Nonempty.product

added theorem Finset.Nonempty.snd

added theorem Finset.card_product

added theorem Finset.coe_offDiag

added theorem Finset.coe_product

added def Finset.diag

added theorem Finset.diag_card

added theorem Finset.diag_empty

added theorem Finset.diag_insert

added theorem Finset.diag_inter

added theorem Finset.diag_mono

added theorem Finset.diag_singleton

added theorem Finset.diag_union

added theorem Finset.diag_union_offDiag

added theorem Finset.disjUnion_product

added theorem Finset.disjoint_diag_offDiag

added theorem Finset.disjoint_product

added theorem Finset.empty_product

added theorem Finset.filter_product

added theorem Finset.filter_product_card

added theorem Finset.filter_product_left

added theorem Finset.filter_product_right

added theorem Finset.image_swap_product

added theorem Finset.inter_product

added theorem Finset.map_swap_product

added theorem Finset.mem_diag

added theorem Finset.mem_offDiag

added theorem Finset.mem_product

added theorem Finset.mk_mem_product

added theorem Finset.nonempty_product

added def Finset.offDiag

added theorem Finset.offDiag_card

added theorem Finset.offDiag_empty

added theorem Finset.offDiag_insert

added theorem Finset.offDiag_inter

added theorem Finset.offDiag_mono

added theorem Finset.offDiag_singleton

added theorem Finset.offDiag_union

added theorem Finset.product_bunionᵢ

added theorem Finset.product_disjUnion

added theorem Finset.product_empty

added theorem Finset.product_eq_bunionᵢ

added theorem Finset.product_eq_bunionᵢ_right

added theorem Finset.product_eq_empty

added theorem Finset.product_image_fst

added theorem Finset.product_image_snd

added theorem Finset.product_inter

added theorem Finset.product_inter_product

added theorem Finset.product_sdiff_diag

added theorem Finset.product_sdiff_offDiag

added theorem Finset.product_singleton

added theorem Finset.product_subset_product

added theorem Finset.product_subset_product_left

added theorem Finset.product_subset_product_right

added theorem Finset.product_union

added theorem Finset.product_val

added theorem Finset.singleton_product

added theorem Finset.singleton_product_singleton

added theorem Finset.subset_product

added theorem Finset.subset_product_image_fst

added theorem Finset.subset_product_image_snd

added theorem Finset.union_product