castHom_comp — Mathlib

English

Given divisibility relations hm: n | m and hd: m | d, the composition of castHoms satisfies (castHom hm n) ∘ (castHom hd m) = castHom (dvd_trans hm hd) n.

Русский

При отношениях делимости hm: n|m и hd: m|d, композиция castHom удовлетворяет (castHom hm n) ∘ (castHom hd m) = castHom (dvd_trans hm hd) n.

LaTeX

$$$(castHom\ hm\ (ZMod\ n)).\mathrm{comp} (castHom\ hd\ (ZMod\ m)) = castHom\ (dvd\_trans\ hm\ hd)\ (ZMod\ n)$$$

Lean4

@[simp]
theorem castHom_comp {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    (castHom hm (ZMod n)).comp (castHom hd (ZMod m)) = castHom (dvd_trans hm hd) (ZMod n) :=
  RingHom.ext_zmod _ _

Похожие утверждения