mathlib3

b013b2d6 - feat(ring_theory): define subsemirings (#2837)

feat(ring_theory): define subsemirings (#2837) ~~Depends on #2836,~~ needs a better module docstring. Some lemmas are missing, most notably `(subsemiring.closure s : set R) = add_submonoid.closure (submonoid.closure s)`.