unitsMap_self

Mathlib.Data.ZMod.Units

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

English

The units map for the identity divisor is the identity map on units.

Русский

Отображение единиц для тождественного делителя равно тождественному отображению на единицах.

LaTeX

$$$$ (unitsMap (dvd\\_refl n)) = MonoidHom.id _ $$$$

Lean4

@[simp]
theorem unitsMap_self (n : ℕ) : unitsMap (dvd_refl n) = MonoidHom.id _ := by simp [unitsMap, castHom_self]

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

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

Разделы

Аффилиация

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