mathlib documentation

data.zmod.algebra

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

@[protected, instance]
def zmod.algebra.subsingleton (R : Type u_1) [ring R] (p : ) :
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
@[protected, instance]
def zmod.algebra (R : Type u_1) [ring R] (p : ) [char_p R p] :
Equations