From 9806b5c30f479bb9e02e4ab75905e26a09206f20 Mon Sep 17 00:00:00 2001 From: "Filippo A. E. Nuccio" Date: Thu, 22 Sep 2022 22:45:37 +0000 Subject: [PATCH] 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 --- src/topology/algebra/filter_basis.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/topology/algebra/filter_basis.lean b/src/topology/algebra/filter_basis.lean index 0f68d87bbddbe..5ef959246ca60 100644 --- a/src/topology/algebra/filter_basis.lean +++ b/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)