Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-31 20:59 4f6307eb

View on Github →

feat(topology/algebra/open_subgroup): basics on open subgroups (#1067)

Dump the file into mathlib
feat(algebra/pi_instances): product of submonoids/groups/rings From the perfectoid project.
Small changes
feat(topology/algebra/open_subgroup): basics on open subgroups
Some proof compression
Update src/topology/algebra/open_subgroup.lean

Estimated changes

Created src/topology/algebra/open_subgroup.lean

added theorem ideal.is_open_of_open_subideal

added theorem open_add_subgroup.coe_inf

added theorem open_add_subgroup.is_open_of_open_add_subgroup

added theorem open_add_subgroup.le_iff

added theorem open_add_subgroup.mem_nhds_zero

added def open_add_subgroup.prod

added theorem open_subgroup.coe_inf

added theorem open_subgroup.coe_injective

added theorem open_subgroup.ext'

added theorem open_subgroup.ext

added theorem open_subgroup.is_closed

added theorem open_subgroup.is_open_of_nonempty_open_subset

added theorem open_subgroup.is_open_of_open_subgroup

added theorem open_subgroup.le_iff

added theorem open_subgroup.mem_nhds_one

added def open_subgroup.prod

added def open_subgroup

added theorem submodule.is_open_of_open_submodule