Documentation

Mathlib.GroupTheory.GroupAction.Ring

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.

source
instance NonUnitalNonAssocSemiring.toDistribSMul {α : Type u_1} [NonUnitalNonAssocSemiring α] :
DistribSMul α α
Equations
source
instance NonUnitalNonAssocSemiring.nat_smulCommClass {α : Type u_1} [NonUnitalNonAssocSemiring α] :
SMulCommClass ℕ α α

Note that AddMonoid.nat_smulCommClass requires stronger assumptions on α.

Equations
  • ⋯ = ⋯
source
instance NonUnitalNonAssocSemiring.nat_isScalarTower {α : Type u_1} [NonUnitalNonAssocSemiring α] :
IsScalarTower ℕ α α

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on α.

Equations
  • ⋯ = ⋯
source
instance NonUnitalNonAssocRing.int_smulCommClass {α : Type u_1} [NonUnitalNonAssocRing α] :
SMulCommClass ℤ α α

Note that AddMonoid.int_smulCommClass requires stronger assumptions on α.

Equations
  • ⋯ = ⋯
source
instance NonUnitalNonAssocRing.int_isScalarTower {α : Type u_1} [NonUnitalNonAssocRing α] :
IsScalarTower ℤ α α

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on α.

Equations
  • ⋯ = ⋯