Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-21 21:29 971ddcc2

View on Github →

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.

Estimated changes