Skip to content

Commit

Permalink
make consistent
Browse files Browse the repository at this point in the history
Co-authored-by: Etienne <[email protected]>
  • Loading branch information
YaelDillies and EtienneC30 authored Feb 12, 2025
1 parent 72b82dc commit aa96fb6
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions Mathlib/MeasureTheory/Group/Measure.lean
Original file line number Diff line number Diff line change
Expand Up @@ -394,6 +394,7 @@ section Group
variable [Group G] {μ : Measure G}

section MeasurableMul

variable [MeasurableMul G]

@[to_additive]
Expand Down

0 comments on commit aa96fb6

Please sign in to comment.