Integer unit signs acting on modules #
The sign action of an integer unit agrees with the action of its image in the scalar ring.
This lets integer signs in the scalar ring, such as powers of -1, combine with integer unit
actions.
theorem
TauCeti.intCast_smul_units_smul
{R : Type u_1}
{V : Type u_2}
[Ring R]
[AddCommGroup V]
[Module R V]
(u' u : ℤˣ)
(v : V)
:
Acting by the image of an integer unit in the scalar ring and then by a second integer unit is the action of their product as integer units.