feat(*): image_closure (#1069)

Commit

6 years ago

feat(*): image_closure (#1069) Prove that the image of the closure is the closure of the image, for submonoids/groups/rings. From the perfectoid project.