mathlib

557f5e5d - feat(algebra/add_monoid_algebra/degree): new file with lemmas about support.sup/inf (#15413)

feat(algebra/add_monoid_algebra/degree): new file with lemmas about support.sup/inf (#15413) This PR contains the initial lemmas that prove basic properties about `finset.support.sup/inf`, with a view towards defining `degree`s for `add_monoid_algebra`s. It is split off from #15296.