Theorems · Definition · number theory

ZMod.castHom

{n m : ℕ} → m ∣ n → (R : Type u_2) → [inst : Ring R] → [CharP R m] → ZMod n →+* R

The canonical ring homomorphism from ZMod n to a ring of characteristic dividing n. See also ZMod.lift for a generalized version working in AddGroups.

Defined in

Mathlib.Data.ZMod.Basic

Cited by

55 results in Mathlib

Foundations

Depth 60 from the axioms · uses propext, Quot.sound

Assumes

RingCharP