mathlib documentation

data.zmod.algebra

The zmod n-algebra structure on rings whose characteristic divides n #

def zmod.algebra' (R : Type u_1) [ring R] {n : } (m : ) [char_p R m] (h : m n) :

The zmod n-algebra structure on rings whose characteristic m divides n

Equations
@[instance]
def zmod.algebra (R : Type u_1) [ring R] (n : ) [char_p R n] :
Equations