changeLevel_trans — Mathlib

English

The changeLevel maps compose: changeLevel(dvd_trans hm hd) χ = changeLevel hd (changeLevel hm χ).

Русский

Сопоставления повышения уровня образуют композицию: изменение уровня по dvd_trans совпадает с последовательностью изменений.

LaTeX

$$$$ changeLevel(\\mathrm{dvd\\_trans}\\ hm\\ hd)\\; χ = changeLevel hd\\; (changeLevel hm\\; χ). $$$$

Lean4

theorem changeLevel_trans {m d : ℕ} (hm : n ∣ m) (hd : m ∣ d) :
    changeLevel (dvd_trans hm hd) χ = changeLevel hd (changeLevel hm χ) := by
  simp [changeLevel_def, MonoidHom.comp_assoc, ZMod.unitsMap_comp]

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