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.

Equations

Note that AddMonoid.nat_smulCommClass requires stronger assumptions on α.

Equations
  • =

Note that AddCommMonoid.nat_isScalarTower requires stronger assumptions on α.

Equations
  • =

Note that AddMonoid.int_smulCommClass requires stronger assumptions on α.

Equations
  • =

Note that AddCommGroup.int_isScalarTower requires stronger assumptions on α.

Equations
  • =