Commutative structures from unbundled commutativity

This file provides scoped instances that promote algebraic structures satisfying IsMulCommutative or IsAddCommutative to their bundled commutative counterparts.

@[instance_reducible]

def IsMulCommutative.instCommMagma {M : Type u_2} [Mul M] [IsMulCommutative M] : CommMagma M

A magma which IsMulCommutative is a CommMagma.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsMulCommutative.instCommMagma = { toMul := inst✝¹, mul_comm := ⋯ }

@[instance_reducible]

def IsAddCommutative.instAddCommMagma {M : Type u_2} [Add M] [IsAddCommutative M] : AddCommMagma M

An additive magma which IsMulCommutative is a AddCommMagma.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsAddCommutative.instAddCommMagma = { toAdd := inst✝¹, add_comm := ⋯ }

@[instance_reducible]

def IsMulCommutative.instCommSemigroup {M : Type u_2} [Semigroup M] [IsMulCommutative M] : CommSemigroup M

A Semigroup which IsMulCommutative is a CommSemigroup.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsMulCommutative.instCommSemigroup = { toSemigroup := inst✝¹, mul_comm := ⋯ }

@[instance_reducible]

def IsAddCommutative.instAddCommSemigroup {M : Type u_2} [AddSemigroup M] [IsAddCommutative M] : AddCommSemigroup M

An AddSemigroup which IsMulCommutative is a AddCommSemigroup.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsAddCommutative.instAddCommSemigroup = { toAddSemigroup := inst✝¹, add_comm := ⋯ }

@[instance_reducible]

def IsMulCommutative.instCommMonoid {M : Type u_2} [Monoid M] [IsMulCommutative M] : CommMonoid M

A Monoid which IsMulCommutative is a CommMonoid.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsMulCommutative.instCommMonoid = { toMonoid := inst✝¹, mul_comm := ⋯ }

@[instance_reducible]

def IsAddCommutative.instAddCommMonoid {M : Type u_2} [AddMonoid M] [IsAddCommutative M] : AddCommMonoid M

A AddMonoid which IsMulCommutative is a AddCommMonoid.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsAddCommutative.instAddCommMonoid = { toAddMonoid := inst✝¹, add_comm := ⋯ }

@[instance_reducible]

def IsMulCommutative.instDivisionCommMonoid {M : Type u_2} [DivisionMonoid M] [IsMulCommutative M] : DivisionCommMonoid M

A DivisionMonoid which IsMulCommutative is a DivisionCommMonoid.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsMulCommutative.instDivisionCommMonoid = { toDivisionMonoid := inst✝¹, mul_comm := ⋯ }

@[instance_reducible]

def IsAddCommutative.instDivisionAddCommMonoid {M : Type u_2} [SubtractionMonoid M] [IsAddCommutative M] : SubtractionCommMonoid M

A SubtractionMonoid which IsMulCommutative is a SubtractionCommMonoid.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsAddCommutative.instDivisionAddCommMonoid = { toSubtractionMonoid := inst✝¹, add_comm := ⋯ }

@[instance_reducible]

def IsMulCommutative.instCommGroup {G : Type u_2} [Group G] [IsMulCommutative G] : CommGroup G

A Group which IsMulCommutative is a CommGroup.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsMulCommutative.instCommGroup = { toGroup := inst✝¹, mul_comm := ⋯ }

@[instance_reducible]

def IsAddCommutative.instAddCommGroup {G : Type u_2} [AddGroup G] [IsAddCommutative G] : AddCommGroup G

An AddGroup which IsMulCommutative is a AddCommGroup.

This is primarily used to deduce the bundled version from the unbundled one for commutative subobjects in a noncommutative ambient type. As such this is only available inside the IsMulCommutative scope so as to avoid deleterious effects to type class synthesis for bundled commutativity.

See note [commutative subobjects].

Equations

• IsAddCommutative.instAddCommGroup = { toAddGroup := inst✝¹, add_comm := ⋯ }