feat(Algebra/Group/Submonoid): type class to indicate that supremum in a SubmonoidClass agrees with supremum of submonoids#39687

TentativeConvert wants to merge 3 commits into

leanprover-community:masterleanprover-community/mathlib4:masterfrom

TentativeConvert:addsubmonoid-ssupTentativeConvert/mathlib4:addsubmonoid-ssupCopy head branch name to clipboard