ZMod n-scalars commute with every additive action

A ZMod n-module structure on an abelian group is unique, and every additive endomorphism is ZMod n-linear for it (ZMod.map_smul). So any distributive action on a ZMod n-module commutes with the ZMod n-scalars. These are the ZMod n counterparts of Mathlib's AddMonoid.nat_smulCommClass and AddGroup.int_smulCommClass, and they supply the linearity hypothesis of a G-module with ZMod n coefficients.

Main results

• TauCeti.ZMod.smulCommClass, TauCeti.ZMod.smulCommClass': a distributive action on a ZMod n-module commutes with the ZMod n-scalars.

instance TauCeti.ZMod.smulCommClass {n : ℕ} {M : Type u_1} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] [DistribSMul M A] : SMulCommClass (ZMod n) M A

A distributive action on a ZMod n-module commutes with the ZMod n-scalars, each operator being additive and hence ZMod n-linear.

instance TauCeti.ZMod.smulCommClass' {n : ℕ} {M : Type u_1} {A : Type u_2} [AddCommGroup A] [Module (ZMod n) A] [DistribSMul M A] : SMulCommClass M (ZMod n) A

A distributive action on a ZMod n-module commutes with the ZMod n-scalars.