changeLevel_eq_cast_of_dvd — Mathlib

English

For hm : n ∣ m and a ∈ Units(ZMod m), (changeLevel hm χ) a = χ(ZMod.cast(a)).

Русский

При hm: n|m и a ∈ Units(ZMod m) выполняется (changeLevel hm χ) a = χ(ZMod.cast(a)).

LaTeX

$$$$ (changeLevel hm χ)\\; a = χ\\bigl(\\mathrm{ZMod.cast}(a)\\bigr) $$$$

Lean4

theorem changeLevel_eq_cast_of_dvd {m : ℕ} (hm : n ∣ m) (a : Units (ZMod m)) :
    (changeLevel hm χ) a = χ (ZMod.cast (a : ZMod m)) := by simp [changeLevel_def, ZMod.unitsMap_val]

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