# Commutativity and associativity of action of integers on rings #

This file proves that `ℕ`

and `ℤ`

act commutatively and associatively on (semi)rings.

## TODO #

Those instances are in their own file only because they require much less imports than any existing file they could go to. This is unfortunate and should be fixed by reorganising files.

instance
NonUnitalNonAssocSemiring.nat_smulCommClass
{α : Type u_1}
[NonUnitalNonAssocSemiring α]
:

SMulCommClass ℕ α α

Note that `AddMonoid.nat_smulCommClass`

requires stronger assumptions on `α`

.

## Equations

- ⋯ = ⋯

instance
NonUnitalNonAssocSemiring.nat_isScalarTower
{α : Type u_1}
[NonUnitalNonAssocSemiring α]
:

IsScalarTower ℕ α α

Note that `AddCommMonoid.nat_isScalarTower`

requires stronger assumptions on `α`

.

## Equations

- ⋯ = ⋯

instance
NonUnitalNonAssocRing.int_smulCommClass
{α : Type u_1}
[NonUnitalNonAssocRing α]
:

SMulCommClass ℤ α α

Note that `AddMonoid.int_smulCommClass`

requires stronger assumptions on `α`

.

## Equations

- ⋯ = ⋯

instance
NonUnitalNonAssocRing.int_isScalarTower
{α : Type u_1}
[NonUnitalNonAssocRing α]
:

IsScalarTower ℤ α α

Note that `AddCommGroup.int_isScalarTower`

requires stronger assumptions on `α`

.

## Equations

- ⋯ = ⋯