mathlib

9806b5c3 - doc(topology/algebra/filter_basis): modify doc of `add_group_filter_basis_of_comm` (#16597)

doc(topology/algebra/filter_basis): modify doc of `add_group_filter_basis_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>