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

• (_ : SMulCommClass ℕ α α) = (_ : SMulCommClass ℕ α α)

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

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on α.

Equations

• (_ : IsScalarTower ℕ α α) = (_ : IsScalarTower ℕ α α)

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

Note that AddMonoid.int_smulCommClass requires stronger assumptions on α.

Equations

• (_ : SMulCommClass ℤ α α) = (_ : SMulCommClass ℤ α α)

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

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on α.

Equations

• (_ : IsScalarTower ℤ α α) = (_ : IsScalarTower ℤ α α)