mathlib

41137fe0 - feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring (#6860)