Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-03-14 00:42 19ecff8b

View on Github →

feat(topology/algebra/nonarchimedean): added nonarchimedean groups and rings (#6551) Adding nonarchimedean topological groups and rings.

Estimated changes

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

added theorem nonarchimedean_group.nonarchimedean_of_emb

added theorem nonarchimedean_group.prod_self_subset

added theorem nonarchimedean_group.prod_subset

added theorem nonarchimedean_ring.left_mul_subset

added theorem nonarchimedean_ring.mul_subset

Modified src/topology/algebra/open_subgroup.lean

added theorem open_subgroup.coe_comap

added def open_subgroup.comap

added theorem open_subgroup.comap_comap

added theorem open_subgroup.mem_comap

Modified src/topology/algebra/ring.lean