refactor: add refactored APIs for algebraic filter bases

[ADedecker]

This is the first part of the refactor of algebraic filter bases discussed here. This adds the new APIs without touching any existing file in order to split the work. Please review this by comparing with the existing API!

See #18202 for the full picture.

---

[github-actions]

PR summary ecfc7661ff

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.Algebra.FilterBasisNew (new file)	1088
Mathlib.Topology.Algebra.Nonarchimedean.BasesNew (new file)	1096

---

Declarations diff

+ HasBasis.isGroupBasis
+ HasBasis.isModuleBasis
+ HasBasis.isRingBasis
+ IsAddGroupBasis
+ IsGroupBasis
+ IsGroupBasis.mk_of_comm
+ IsModuleBasis
+ IsModuleBasis.mk_of_hasBasis
+ IsRingBasis
+ IsRingBasis.mk_of_comm
+ continuousSMul_of_hasBasis
+ instance (priority := 100) continuousConstSMul :
+ instance (priority := 100) continuousSMul [TopologicalRing R] :
+ instance (priority := 100) topologicalGroup :
+ instance (priority := 100) topologicalRing :
+ 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

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.

---

Increase in tech debt: (relative, absolute) = (1.00, 0.00)

Current number	Change	Type
5012	1	porting notes

Current commit ecfc7661ff
Reference commit 675c28ea28

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).