Commit 2023-01-16 17:38 2cd9351d

View on Github →

feat: port Data.Finset.Pi (#1590)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Pi.lean

added def Finset.Pi.empty

added theorem Finset.mem_pi

added def Finset.pi.cons

added theorem Finset.pi.cons_ne

added theorem Finset.pi.cons_same

added theorem Finset.pi_cons_injective

added theorem Finset.pi_const_singleton

added theorem Finset.pi_disjoint_of_disjoint

added theorem Finset.pi_empty

added theorem Finset.pi_insert

added theorem Finset.pi_singletons

added theorem Finset.pi_subset

added theorem Finset.pi_val