Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2018-11-05 09:03 8ae3fb86

View on Github →

feat(ring_theory/subring): ring.closure (#444)

Estimated changes

Modified group_theory/subgroup.lean

added theorem add_group.in_closure.rec_on

Modified group_theory/submonoid.lean

added theorem add_monoid.in_closure.rec_on

Modified ring_theory/subring.lean

added def ring.closure

added theorem ring.closure_subset

added theorem ring.closure_subset_iff

added theorem ring.exists_list_of_mem_closure

added theorem ring.mem_closure

added theorem ring.subset_closure