Commit 2023-01-17 19:16 5695e6d9

View on Github →

feat: port Data.FinEnum (#1607)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/FinEnum.lean

added def FinEnum.Finset.enum

added theorem FinEnum.Finset.mem_enum

added def FinEnum.Pi.cons

added def FinEnum.Pi.tail

added theorem FinEnum.mem_pi

added theorem FinEnum.mem_toList

added theorem FinEnum.nodup_toList

added def FinEnum.ofEquiv

added def FinEnum.ofList

added def FinEnum.ofNodupList

added def FinEnum.ofSurjective

added def FinEnum.pi.enum

added theorem FinEnum.pi.mem_enum

added def FinEnum.pi

added def FinEnum.toList