mathlib3

b00d9bec - chore(data/finset/basic, ring_theory/hahn_series): mostly namespace changes (#6996)

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 Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>