isUnit_cast_of_dvd

Mathlib.Data.ZMod.Units

URI: https://scilib.ai/kg/mathlib#ZMod.isUnit_cast_of_dvd

English

If n divides m and a is a unit in ZMod m, then its cast to ZMod n is a unit.

Русский

Если n делит m и a — единица в ZMod m, то её приведение к ZMod n также единица.

LaTeX

$$$$ (hm : n \\mid m) \\; (a : (ZMod m)^{\\times}) \\Rightarrow IsUnit (cast (a : ZMod m) : ZMod n) $$$$

Lean4

theorem isUnit_cast_of_dvd (hm : n ∣ m) (a : Units (ZMod m)) : IsUnit (cast (a : ZMod m) : ZMod n) :=
  Units.isUnit (unitsMap hm a)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru