From aa96fb64d7b873f78d4a1cd31b75fcbac29bcb35 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Wed, 12 Feb 2025 22:35:00 +0100 Subject: [PATCH] make consistent Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com> --- Mathlib/MeasureTheory/Group/Measure.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/MeasureTheory/Group/Measure.lean b/Mathlib/MeasureTheory/Group/Measure.lean index 5c7608e467f9a..6c30a4f66e120 100644 --- a/Mathlib/MeasureTheory/Group/Measure.lean +++ b/Mathlib/MeasureTheory/Group/Measure.lean @@ -394,6 +394,7 @@ section Group variable [Group G] {μ : Measure G} section MeasurableMul + variable [MeasurableMul G] @[to_additive]