You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Both data/set/finite and data/fintype/basic have lemmas involving set.to_finset, and it seems there is no organizational principle behind this.
As suggested by @b-mehtahere, these should be moved to data/fintype/basic. (The linked PR contributes to the problem, so this issue is a reminder to get to dealing with it.)
The text was updated successfully, but these errors were encountered:
Both
data/set/finite
anddata/fintype/basic
have lemmas involvingset.to_finset
, and it seems there is no organizational principle behind this.As suggested by @b-mehta here, these should be moved to
data/fintype/basic
. (The linked PR contributes to the problem, so this issue is a reminder to get to dealing with it.)The text was updated successfully, but these errors were encountered: