Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 14:26 7f837db4

View on Github →

feat(data/set/finite): add multiset.finite_to_set (#15177)

  • move finset.finite_to_set up;
  • add multiset.finite_to_set, multiset.finite_to_set_to_finset, and list.finite_to_set;
  • use new lemmas here and there.

Estimated changes

modified theorem finset.finite_to_set
added theorem list.finite_to_set
added theorem multiset.finite_to_set