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

instance ZMod.instSubsingletonAlgebra (R : Type u_1) [Ring R] (p : ℕ) : Subsingleton (Algebra (ZMod p) R)

@[reducible, inline]

abbrev ZMod.algebra' (R : Type u_1) [Ring R] {n : ℕ} (m : ℕ) [CharP 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

• ZMod.algebra' R m h = { smul := fun (a : ZMod n) (r : R) => a.cast * r, algebraMap := ZMod.castHom h R, commutes' := ⋯, smul_def' := ⋯ }

@[reducible, inline]

abbrev ZMod.algebra (R : Type u_1) [Ring R] (p : ℕ) [CharP 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

• ZMod.algebra R p = ZMod.algebra' R p ⋯

@[instance_reducible]

def ZMod.algebraOfModule (n : ℕ) (R : Type u_2) [Ring R] [Module (ZMod n) R] : Algebra (ZMod n) R

Any ring with a ZMod p-module structure can be upgraded to a ZMod p-algebra. Not an instance because this is usually not the default way, and this will cause typeclass search loop.

Equations

• ZMod.algebraOfModule n R = Algebra.ofModule' ⋯ ⋯

theorem ZMod.algebraOfModule.proof (n : ℕ) (R : Type u_2) [Ring R] [Module (ZMod n) R] (r : ZMod n) (x : R) : r • 1 * x = r • x ∧ x * r • 1 = r • x

instance ZMod.instIsScalarTower (n : ℕ) (R : Type u_2) (M : Type u_3) [Ring R] [AddCommGroup M] [Module (ZMod n) R] [m₁ : Module (ZMod n) M] [Module R M] : IsScalarTower (ZMod n) R M