Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-10 06:34 9e288527

View on Github →

feat(field_theory/krull_topology): added krull_topology_totally_disconnected (#12398)

Estimated changes

Modified src/field_theory/krull_topology.lean

added theorem intermediate_field.fixing_subgroup_is_closed

modified theorem krull_topology_t2

added theorem krull_topology_totally_disconnected

deleted theorem subgroup.is_open_of_one_mem_interior

Modified src/topology/algebra/open_subgroup.lean

modified theorem subgroup.is_open_mono

added theorem subgroup.is_open_of_one_mem_interior

Modified src/topology/connected.lean

added theorem is_totally_disconnected_of_clopen_set