mathlib

d655f459 - feat(topology/algebra/filter_basis): add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group (#14806)

feat(topology/algebra/filter_basis): add a variant of `module_filter_basis.has_continuous_smul` when we already have a topological group (#14806) This basically just factors the existing proof to get for free that it works not only for the topology generated by the basis (as an `add_group_filter_basis`) but for any topological add group topology with a suitable basis of neighborhoods of 0. This adds nothing new mathematically because group topologies are characterized by their neighborhoods of 0, so one could obtain such a result by building a second topology from the filter basis and proving it is equal to the first one, but it turns out it's just easier to split the proof, so this is just a free quality-of-life improvement.