Commit 2023-01-20 09:37 9793a3b2

View on Github →

feat: Port data.fintype.sort (#1690) Port of data.fintype.sort No changes except docu fixes

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Fintype/Sort.lean

added def finSumEquivOfFinset

added theorem finSumEquivOfFinset_inl

added theorem finSumEquivOfFinset_inr

added def monoEquivOfFin