@[protected, instance]
The zmod n-algebra structure on rings whose characteristic m divides n
Equations
- zmod.algebra' R m h = {to_has_smul := {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 p = zmod.algebra' R p dvd_rfl