English
If n | m and m | d, then the composition of the CastHom maps (castHom n ⟶ m) and (castHom m ⟶ d) is equal to the CastHom n ⟶ d corresponding to the transitive divisor relation: castHom n ⟶ d.
Русский
Если n делится на m и m делится на d, то композиция отображений castHom соответствует транзитивному делителю: castHom n ⟶ d.
LaTeX
$$$ castHom\; hm\; (ZMod n) \circ castHom\; hd\; (ZMod m) = castHom\; (dvd\_trans\; hm\; hd) \; (ZMod n)$$$
Lean4
theorem ext_zmod {n : ℕ} {R : Type*} [NonAssocSemiring R] (f g : ZMod n →+* R) : f = g :=
by
ext a
obtain ⟨k, rfl⟩ := ZMod.intCast_surjective a
let φ : ℤ →+* R := f.comp (Int.castRingHom (ZMod n))
let ψ : ℤ →+* R := g.comp (Int.castRingHom (ZMod n))
change φ k = ψ k
rw [φ.ext_int ψ]
