diff --git a/Mathlib/Algebra/Group/Commutator.lean b/Mathlib/Algebra/Group/Commutator.lean index e0b0b3d11fa884..f6fb3c2445b6b9 100644 --- a/Mathlib/Algebra/Group/Commutator.lean +++ b/Mathlib/Algebra/Group/Commutator.lean @@ -34,6 +34,12 @@ attribute [scoped instance] commutatorElement end commutatorElement +namespace addCommutatorElement + +attribute [scoped instance] addCommutatorElement + +end addCommutatorElement + open scoped commutatorElement @[to_additive]