Commit 2024-10-25 09:55 8e419e3d

View on Github →

feat (Data/Finset/Basic) : Equivalence between Pi type over Finset.cons and a product (#17004) This PR defines an equivalence between Pi over an augmented finset and a product with Pi over the original finset.

Estimated changes

Modified Mathlib/Data/Finset/Basic.lean

added def Finset.consPiProd

added def Finset.consPiProdEquiv

added theorem Finset.eq_of_mem_cons_of_not_mem

added theorem Finset.eq_of_mem_insert_of_not_mem

deleted theorem Finset.eq_of_not_mem_of_mem_insert

added def Finset.insertPiProd

added def Finset.insertPiProdEquiv

added theorem Finset.mem_of_mem_cons_of_ne

added def Finset.prodPiCons

added def Finset.prodPiInsert

Modified Mathlib/GroupTheory/SpecificGroups/KleinFour.lean

Modified Mathlib/Order/CountableDenseLinearOrder.lean