Commit 2023-03-17 16:27 447e000d

View on Github →

feat: port Topology.Algebra.Nonarchimedean.Basic (#2958)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/Nonarchimedean/Basic.lean

added theorem NonarchimedeanGroup.nonarchimedean_of_emb

added theorem NonarchimedeanGroup.prod_self_subset

added theorem NonarchimedeanGroup.prod_subset

added theorem NonarchimedeanRing.left_mul_subset

added theorem NonarchimedeanRing.mul_subset