Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-15 14:32 83f81aea

View on Github →

refactor(topology/algebra/open_subgroup): use set_like (#18585)

Estimated changes

Modified src/field_theory/krull_topology.lean

Modified src/topology/algebra/nonarchimedean/basic.lean

Modified src/topology/algebra/open_subgroup.lean

added theorem open_subgroup.coe_coe_opens

added theorem open_subgroup.coe_coe_subgroup

deleted theorem open_subgroup.coe_injective

added theorem open_subgroup.coe_opens_inf

added theorem open_subgroup.coe_opens_top

added theorem open_subgroup.coe_prod

added theorem open_subgroup.coe_subgroup_comap

added theorem open_subgroup.coe_subgroup_inf

added theorem open_subgroup.coe_subgroup_injective

added theorem open_subgroup.coe_subgroup_prod

added theorem open_subgroup.coe_subgroup_sup

added theorem open_subgroup.coe_subgroup_top

deleted theorem open_subgroup.coe_subset

added theorem open_subgroup.coe_top

modified def open_subgroup.comap

modified theorem open_subgroup.ext

deleted theorem open_subgroup.ext_iff

added theorem open_subgroup.is_clopen

deleted theorem open_subgroup.mem_coe

added theorem open_subgroup.mem_inf

added theorem open_subgroup.mem_top

modified theorem subgroup.is_open_of_one_mem_interior

modified theorem subgroup.is_open_of_open_subgroup