Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-25 09:58 4db21255

View on Github →

feat(group_theory/submonoid): add *.of_mclosure_eq_top (#16985)

add is_scalar_tower.of_mclosure_eq_top and smul_comm_class.of_mclosure_eq_top;
golf submonoid.closure_comm_monoid_of_comm;
add con.mrange_mk'.

Estimated changes

Modified src/group_theory/congruence.lean

added theorem con.mrange_mk'

Modified src/group_theory/submonoid/membership.lean

added theorem is_scalar_tower.of_mclosure_eq_top

added theorem smul_comm_class.of_mclosure_eq_top

modified def submonoid.closure_comm_monoid_of_comm