unitsMap_def

Mathlib.Data.ZMod.Units

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

English

The map unitsMap hm is equal to the image map Units.map under castHom hm (ZMod n).

Русский

Отображение unitsMap hm равно отображению Units.map под отображением castHom hm (ZMod n).

LaTeX

$$$$ unitsMap\\ hm = Units.map (castHom hm (ZMod n)). $$$$

Lean4

theorem unitsMap_def (hm : n ∣ m) : unitsMap hm = Units.map (castHom hm (ZMod n)) :=
  rfl

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

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

Разделы

Аффилиация

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