Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-04-10 13:58 4a155031

View on Github →

refactor(ring_theory): unify monoid closure in ring theory with the one in group theory

Estimated changes

Modified group_theory/submonoid.lean

added theorem monoid.closure_subset

deleted theorem monoid.is_submonoid_closure

added theorem monoid.subset_closure

Modified ring_theory/localization.lean

deleted def localization.closure

deleted inductive localization.in_closure

deleted theorem localization.subset_closure