The zmod n-algebra structure on rings whose characteristic m divides n
Equations
- zmod.algebra' R m h = {to_has_scalar := {smul := λ (a : zmod n) (r : R), (↑a) * r}, to_ring_hom := {to_fun := (zmod.cast_hom h R).to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
@[protected, instance]
Equations
- zmod.algebra R n = zmod.algebra' R n _