mathlib3 documentation

data.zmod.algebra

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

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

@[protected, instance]
def zmod.algebra.subsingleton (R : Type u_1) [ring R] (p : ) :
@[reducible]
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. See note [reducible non-instances].

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

The zmod p-algebra structure on a ring of characteristic p. This is not an instance since it creates a diamond with algebra.id. See note [reducible non-instances].

Equations