unitsMap_val — Mathlib

English

The coercion of a unit under unitsMap equals the underlying cast of the image in ZMod n.

Русский

Приведение единицы через unitsMap равняется изображению в ZMod n через приведение к значениям.

LaTeX

$$$$ ↑(unitsMap hm a) = ((a : ZMod m).cast : ZMod n) $$$$

Lean4

/-- `unitsMap_val` shows that coercing from `(ZMod m)ˣ` to `ZMod n` gives the same result
when going via `(ZMod n)ˣ` and `ZMod m`. -/
theorem unitsMap_val (h : n ∣ m) (a : (ZMod m)ˣ) : ↑(unitsMap h a) = ((a : ZMod m).cast : ZMod n) :=
  rfl

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