@@ -1285,15 +1285,128 @@ class IsMulCommutative (M : Type*) [Mul M] : Prop where
12851285 is_comm : Std.Commutative (α := M) (· * ·)
12861286
12871287@[to_additive]
1288- instance (priority := 100 ) CommMonoid.ofIsMulCommutative {M : Type *} [Monoid M]
1289- [IsMulCommutative M] :
1290- CommMonoid M where
1291- mul_comm := IsMulCommutative.is_comm.comm
1288+ lemma isMulCommutative_iff {M : Type *} [Mul M] :
1289+ IsMulCommutative M ↔ ∀ a b : M, a * b = b * a := by
1290+ grind [IsMulCommutative, Std.Commutative]
12921291
12931292@[to_additive]
1294- instance (priority := 100 ) CommGroup.ofIsMulCommutative {G : Type *} [Group G] [IsMulCommutative G] :
1293+ alias ⟨_, IsMulCommutative.of_comm⟩ := isMulCommutative_iff
1294+
1295+ /-- An alternative to `mul_comm` which uses the mixin `IsMulCommutative` instead of bundled
1296+ commutative algebraic structures. In general, you should prefer `mul_comm` unless you are working
1297+ with commutative subobjects in a noncommutative algebraic structure. -/
1298+ @ [to_additive
1299+ /-- An alternative to `add_comm` which uses the mixin `IsAddCommutative` instead of bundled
1300+ commutative algebraic structures. In general, you should prefer `add_comm` unless you are working
1301+ with commutative subobjects in a noncommutative algebraic structure. -/ ]
1302+ lemma mul_comm' {M : Type *} [Mul M] [IsMulCommutative M] (a b : M) : a * b = b * a :=
1303+ IsMulCommutative.is_comm.comm ..
1304+
1305+ namespace IsMulCommutative
1306+
1307+ /-- A magma which `IsMulCommutative` is a `CommMagma`.
1308+
1309+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1310+ subobjects in a noncommutative ambient type. As such this is only available inside the
1311+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1312+ commutativity.
1313+
1314+ See note [commutative subobjects]. -/
1315+ @ [to_additive
1316+ /-- An additive magma which `IsMulCommutative` is a `AddCommMagma`.
1317+
1318+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1319+ subobjects in a noncommutative ambient type. As such this is only available inside the
1320+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1321+ commutativity.
1322+
1323+ See note [commutative subobjects]. -/ ]
1324+ scoped instance (priority := 50 ) {M : Type *} [Mul M] [IsMulCommutative M] :
1325+ CommMagma M where
1326+ mul_comm := IsMulCommutative.is_comm.comm
1327+
1328+ /-- A `Semigroup` which `IsMulCommutative` is a `CommSemigroup`.
1329+
1330+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1331+ subobjects in a noncommutative ambient type. As such this is only available inside the
1332+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1333+ commutativity.
1334+
1335+ See note [commutative subobjects]. -/
1336+ @ [to_additive
1337+ /-- An `AddSemigroup` which `IsMulCommutative` is a `AddCommSemigroup`.
1338+
1339+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1340+ subobjects in a noncommutative ambient type. As such this is only available inside the
1341+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1342+ commutativity.
1343+
1344+ See note [commutative subobjects]. -/ ]
1345+ scoped instance (priority := 50 ) {M : Type *} [Semigroup M] [IsMulCommutative M] :
1346+ CommSemigroup M where
1347+
1348+ /-- A `Monoid` which `IsMulCommutative` is a `CommMonoid`.
1349+
1350+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1351+ subobjects in a noncommutative ambient type. As such this is only available inside the
1352+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1353+ commutativity.
1354+
1355+ See note [commutative subobjects]. -/
1356+ @ [to_additive
1357+ /-- A `AddMonoid` which `IsMulCommutative` is a `AddCommMonoid`.
1358+
1359+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1360+ subobjects in a noncommutative ambient type. As such this is only available inside the
1361+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1362+ commutativity.
1363+
1364+ See note [commutative subobjects]. -/ ]
1365+ scoped instance (priority := 50 ) {M : Type *} [Monoid M] [IsMulCommutative M] :
1366+ CommMonoid M where
1367+
1368+ /-- A `DivisionMonoid` which `IsMulCommutative` is a `DivisionCommMonoid`.
1369+
1370+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1371+ subobjects in a noncommutative ambient type. As such this is only available inside the
1372+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1373+ commutativity.
1374+
1375+ See note [commutative subobjects]. -/
1376+ @ [to_additive
1377+ /-- A `SubtractionMonoid` which `IsMulCommutative` is a `SubtractionCommMonoid`.
1378+
1379+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1380+ subobjects in a noncommutative ambient type. As such this is only available inside the
1381+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1382+ commutativity.
1383+
1384+ See note [commutative subobjects]. -/ ]
1385+ scoped instance (priority := 50 ) {M : Type *} [DivisionMonoid M] [IsMulCommutative M] :
1386+ DivisionCommMonoid M where
1387+
1388+ /-- A `Group` which `IsMulCommutative` is a `CommGroup`.
1389+
1390+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1391+ subobjects in a noncommutative ambient type. As such this is only available inside the
1392+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1393+ commutativity.
1394+
1395+ See note [commutative subobjects]. -/
1396+ @ [to_additive
1397+ /-- An `AddGroup` which `IsMulCommutative` is a `AddCommGroup`.
1398+
1399+ This is primarily used to deduce the bundled version from the unbundled one for commutative
1400+ subobjects in a noncommutative ambient type. As such this is only available inside the
1401+ `IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
1402+ commutativity.
1403+
1404+ See note [commutative subobjects]. -/ ]
1405+ scoped instance (priority := 50 ) {G : Type *} [Group G] [IsMulCommutative G] :
12951406 CommGroup G where
12961407
1408+ end IsMulCommutative
1409+
12971410end IsCommutative
12981411
12991412/-! We initialize all projections for `@[simps]` here, so that we don't have to do it in later
0 commit comments