Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-04-06 18:32 41137fe0

View on Github →

feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring (#6860) This file is extracted from PR #6705

Estimated changes

Modified src/group_theory/submonoid/membership.lean

added theorem submonoid.mul_left_mem_add_closure

added theorem submonoid.mul_mem_add_closure

added theorem submonoid.mul_right_mem_add_closure

Modified src/ring_theory/subsemiring.lean

added def submonoid.subsemiring_closure

added theorem submonoid.subsemiring_closure_coe

added theorem submonoid.subsemiring_closure_eq_closure

added theorem submonoid.subsemiring_closure_to_add_submonoid

added theorem subsemiring.closure_add_submonoid_closure

added theorem subsemiring.closure_submonoid_closure

added theorem subsemiring.coe_closure_eq