mathlib3

806b72b8 - feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring