Commit 2021-04-03 03:51 b00d9bec
View on Github →chore(data/finset/basic, ring_theory/hahn_series): mostly namespace changes (#6996)
Added the line open finset and removed unneccesary finset.s from ring_theory/hahn_series
Added a small lemma to data.finset.basic that will be useful for an upcoming Hahn series PR