Commit 2023-05-08 11:53 afde67a2

View on Github →

feat port: Topology.Algebra.Nonarchimedean.AdicTopology (#3826)

Estimated changes

Modified Mathlib.lean

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

added def Ideal.adicModuleTopology

added def Ideal.adicTopology

added theorem Ideal.adic_basis

added theorem Ideal.adic_module_basis

added theorem Ideal.hasBasis_nhds_adic

added theorem Ideal.hasBasis_nhds_zero_adic

added theorem Ideal.nonarchimedean

added def Ideal.openAddSubgroup

added def Ideal.ringFilterBasis

added def IsAdic

added def WithIdeal.topologicalSpaceModule

added theorem isAdic_iff

added theorem is_bot_adic_iff

added theorem is_ideal_adic_pow