Commit 2023-01-16 17:32 188ebc7d

View on Github →

feat port : Data.Finset.Fin (#1597)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Finset/Fin.lean

added def Finset.attachFin

added theorem Finset.card_attachFin

added theorem Finset.mem_attachFin