Commit 2023-04-17 14:54 6afed5e6

View on Github →

feat: port Topology.Algebra.Nonarchimedean.Bases (#3476)

Estimated changes

Modified Mathlib.lean

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

added structure RingFilterBasis.SubmodulesBasis

added def RingFilterBasis.moduleFilterBasis

added theorem RingFilterBasis.submodulesBasisIsBasis

added theorem RingSubgroupsBasis.hasBasis_nhds

added theorem RingSubgroupsBasis.hasBasis_nhds_zero

added theorem RingSubgroupsBasis.mem_addGroupFilterBasis

added theorem RingSubgroupsBasis.mem_addGroupFilterBasis_iff

added theorem RingSubgroupsBasis.nonarchimedean

added theorem RingSubgroupsBasis.of_comm

added def RingSubgroupsBasis.openAddSubgroup

added def RingSubgroupsBasis.toRingFilterBasis

added def RingSubgroupsBasis.topology

added structure RingSubgroupsBasis

added theorem SubmodulesBasis.nonarchimedean

added def SubmodulesBasis.openAddSubgroup

added def SubmodulesBasis.toModuleFilterBasis

added def SubmodulesBasis.topology

added structure SubmodulesBasis

added theorem SubmodulesRingBasis.toRing_subgroups_basis

added theorem SubmodulesRingBasis.toSubmodulesBasis

added def SubmodulesRingBasis.topology

added structure SubmodulesRingBasis

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