Commit 2023-01-30 00:44 1eee8170

View on Github →

feat: Port/Data.FunLike.Fintype (#1933) port of data.fun_like.fintype

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/FunLike/Fintype.lean

added theorem FunLike.finite'

added theorem FunLike.finite