Commit 2023-09-26 11:46 4d91cd8b

View on Github →

feat: lemmas about finset (#7337) From the marginal project

Estimated changes

Modified Mathlib/Algebra/BigOperators/Option.lean

added theorem Finset.mul_prod_eq_prod_insertNone

Modified Mathlib/Data/Finset/Card.lean

added theorem Finset.cast_card_erase_of_mem

Modified Mathlib/Data/Fintype/Basic.lean

added theorem Finset.image_univ_equiv

added theorem Finset.insert_compl_insert

Modified Mathlib/Data/Fintype/Card.lean

added theorem card_add_card_compl

added theorem card_compl_add_card