Mathlib v3 is deprecated. Go to Mathlib v4

Theorem mul_mem_class.mul_right_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) …
Added mul_mem_class.mul_right_mem_add_closureView on Github →