Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-01 15:29 3fb051dc

View on Github →

feat(field_theory/krull_topology): added krull_topology_t2 (#11973)

Estimated changes

Modified src/data/fun_like/basic.lean

added theorem fun_like.exists_ne

Modified src/field_theory/krull_topology.lean

added theorem intermediate_field.fixing_subgroup_is_open

added theorem krull_topology_t2

added theorem subgroup.is_open_of_one_mem_interior