refactor(AdicTopology): use new API for algebraic filter bases, and factor some code

[ADedecker]

---

• depends on: refactor: add refactored APIs for algebraic filter bases #18437

[github-actions]

PR summary 73b11a3227

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology	1139	1138	-1 (-0.09%)

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.Nonarchimedean.AdicTopology	-1
Mathlib.Topology.Algebra.FilterBasisNew	1062
Mathlib.Topology.Algebra.Nonarchimedean.BasesNew	1070

---

Declarations diff

+ HasBasis.isGroupBasis
+ HasBasis.isModuleBasis
+ HasBasis.isRingBasis
+ Ideal.adicBasis_eq
+ Ideal.adicBasis_isModuleBasis
+ Ideal.adicBasis_isRingBasis
+ Ideal.isAdic_adicTopology
+ IsAddGroupBasis
+ IsAdic.continuousSMul
+ IsAdic.hasBasis_nhds
+ IsAdic.hasBasis_nhds_zero
+ IsAdic.nonarchimedeanAddGroup
+ IsAdic.nonarchimedeanRing
+ IsAdic.openAddSubgroup
+ IsAdic.pow
+ IsAdic.topologicalAddGroup
+ IsAdic.topologicalRing
+ IsGroupBasis
+ IsGroupBasis.mk_of_comm
+ IsModuleBasis
+ IsModuleBasis.mk_of_hasBasis
+ IsRingBasis
+ IsRingBasis.mk_of_comm
+ N
+ N_one
+ adicBasis
+ adicBasis_def
+ adicBasis_isAddGroupBasis
+ adicBasis_isBasis
+ continuousSMul_of_hasBasis
+ hasBasis_N
+ instance (priority := 100) Ideal.instContinuousSMul_adic (I : Ideal R) (M : Type*)
+ instance (priority := 100) Ideal.instNonarchimedeanAddGroup_adic
+ instance (priority := 100) Ideal.instNonarchimedeanRing_adic :
+ instance (priority := 100) Ideal.instTopologicalAddGroup_adic
+ instance (priority := 100) Ideal.instTopologicalRing_adic :
+ instance (priority := 100) continuousConstSMul :
+ instance (priority := 100) continuousSMul [TopologicalRing R] :
+ instance (priority := 100) topologicalGroup :
+ instance (priority := 100) topologicalRing :
+ isAdic
+ isAdic_bot_iff
+ isAdic_iff_hasBasis_nhds_zero
+ mem_nhds_one
+ mk_of_ideals_of_comm
+ mk_of_submodules
+ mk_of_submodules_of_hasBasis
+ nhds_eq
+ nhds_hasBasis
+ nhds_one_eq
+ nhds_one_hasBasis
+ openSubgroup_of_subgroups
+ topologicalGroup_of_hasBasis
+ topologicalRing_of_hasBasis
+ topology'
++ mk_of_subgroups
++ mk_of_subgroups_of_comm
++ nonarchimedean_of_subgroups
+++ topology
- adicModuleTopology
- adic_basis
- adic_module_basis
- hasBasis_nhds_adic
- hasBasis_nhds_zero_adic
- instance (priority := 100) : NonarchimedeanRing R
- is_bot_adic_iff
- is_ideal_adic_pow
- nonarchimedean
- openAddSubgroup
- ringFilterBasis

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• refactor: add refactored APIs for algebraic filter bases #18437
  By Dependent Issues (🤖). Happy coding!