Mathlib v3 is deprecated. Go to Mathlib v4

Theorem smul_comm_class.of_mclosure_eq_top

Modification history

2022-10-25 09:58
src/group_theory/submonoid/membership.lean
feat(group_theory/submonoid): add `*.of_mclosure_eq_top` (#16985) …
Added smul_comm_class.of_mclosure_eq_topView on Github →