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.

source
@[protected, instance]
def zmod.algebra.subsingleton (R : Type u_1) [ring R] (p : ℕ) :
subsingleton (algebra (zmod p) R)
source
@[reducible]
def zmod.algebra' (R : Type u_1) [ring R] {n : ℕ} (m : ℕ) [char_p R m] (h : m ∣ n) :
algebra (zmod n) R

The zmod n-algebra structure on rings whose characteristic m divides n. See note [reducible non-instances].

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

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