doc(topology/algebra/filter_basis): modify doc of `add_group_filter_b…

…asis_of_comm` (#16597)

Added the `additive` adjective to the doc for the @additive variation `add_group_filter_basis_of_comm` of `group_filter_basis_of_comm`



Co-authored-by: Kyle Miller <kmill31415@gmail.com>

src/topology/algebra/filter_basis.lean

@@ -67,7 +67,7 @@ attribute [to_additive] group_filter_basis.conj'
 attribute [to_additive] group_filter_basis.to_filter_basis
 
 /-- `group_filter_basis` constructor in the commutative group case. -/
-@[to_additive "`add_group_filter_basis` constructor in the commutative group case."]
+@[to_additive "`add_group_filter_basis` constructor in the additive commutative group case."]
 def group_filter_basis_of_comm {G : Type*} [comm_group G]
   (sets                   : set (set G))
   (nonempty               : sets.nonempty)