Documentation

Mathlib.Data.ZMod.Algebra

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

instance ZMod.instSubsingletonAlgebra (R : Type u_1) [Ring R] (p : ) :
Equations
  • =
@[reducible, inline]
abbrev ZMod.algebra' (R : Type u_1) [Ring R] {n : } (m : ) [CharP R m] (h : m n) :

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

Equations
Instances For
    @[reducible, inline]
    abbrev ZMod.algebra (R : Type u_1) [Ring R] (p : ) [CharP 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
    Instances For