Commit 2023-01-17 13:28 5f2b48d1

View on Github →

feat: Port Data.Fintype.Sigma (#1625)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Sigma.lean

added theorem Finset.univ_sigma_univ