Commit 2021-01-25 17:49 3a16e9f8
View on Github →feat(data/set/finite): add to_finset lemma (#5883) Add lemma stating that taking to_finset of the union of two sets is the same as taking the union of to_finset of the sets.
feat(data/set/finite): add to_finset lemma (#5883) Add lemma stating that taking to_finset of the union of two sets is the same as taking the union of to_finset of the sets.