Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-11 03:45 c8243a6a

View on Github →

feat(group_theory/submonoid/basic): add monoid_hom.of_mclosure_eq_top_left (#16809)

rename monoid_hom.of_mdense to monoid_hom.of_mclosure_eq_top_right;
add monoid_hom.of_mclosure_eq_top_left.

Estimated changes

Modified src/group_theory/submonoid/basic.lean

added theorem monoid_hom.coe_of_mclosure_eq_top_left

added theorem monoid_hom.coe_of_mclosure_eq_top_right

deleted theorem monoid_hom.coe_of_mdense

added def monoid_hom.of_mclosure_eq_top_left

added def monoid_hom.of_mclosure_eq_top_right

deleted def monoid_hom.of_mdense