Mathlib v3 is deprecated. Go to Mathlib v4

Theorem submonoid.mul_mem_add_closure

Modification history

2022-04-28 17:35
src/group_theory/submonoid/membership.lean
feat(ring_theory/submonoid/membership): generalize a few lemmas to `mul_mem_class` (#13748) …
Deleted submonoid.mul_mem_add_closureView on Github →
2021-04-06 18:32
src/group_theory/submonoid/membership.lean
feat(algebra/add_submonoid_closure): the additive closure of a multiplicative submonoid is a subsemiring (#6860) …
Added submonoid.mul_mem_add_closureView on Github →