Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-16 21:43 214b8e84

View on Github →

feat(topology/algebra): more on closure (#6675)

Estimated changes

Modified src/group_theory/subgroup.lean

added theorem subgroup.inv_coe_set

Created src/topology/algebra/algebra.lean

added theorem subalgebra.is_closed_topological_closure

added theorem subalgebra.subring_topological_closure

added def subalgebra.topological_closure

added theorem subalgebra.topological_closure_minimal

Modified src/topology/algebra/group.lean

added theorem subgroup.is_closed_topological_closure

added theorem subgroup.subgroup_topological_closure

modified def subgroup.topological_closure

added theorem subgroup.topological_closure_minimal

Modified src/topology/algebra/module.lean

Modified src/topology/algebra/monoid.lean

Modified src/topology/algebra/ring.lean

added theorem subring.is_closed_topological_closure

added theorem subring.subring_topological_closure

added def subring.topological_closure

added theorem subring.topological_closure_minimal

added theorem subsemiring.is_closed_topological_closure

added theorem subsemiring.subring_topological_closure

added def subsemiring.topological_closure

added theorem subsemiring.topological_closure_minimal