Mathlib Changelog
Changelog
About
Github
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